In this notebook, we'll look into modelling implied trading within an exchange. Implied trading refers to ability to connect liquidity on strategy and outright order books (e.g. Euronext).

1 Type definitions and printers

1.1 Model type definitions

Our first goal is to setup the various type definitions that we'll use later on.

In [1]:
type side = BUY | SELL

type outright_id = OUT1 | OUT2 | OUT3
type strategy_id = STRAT1 | STRAT2
type month = Mar | Jun | Sep | Dec

(* Map an outright with an expiry *)
let contract_expiry = function
  | OUT1 -> Mar
  | OUT2 -> Jun
  | OUT3 -> Sep

(* Convert month to an integer *)
let month_to_int = function
  | Mar -> 3
  | Jun -> 6
  | Sep -> 9
  | Dec -> 12
;;

(* Return true of m1 is nearer (or equal) to m2 *)
let month_comp (m1 : month) (m2 : month) =
  (month_to_int m1) < (month_to_int  m2)
;;

type instrument =
  | Strategy of strategy_id
  | Outright of outright_id

(* Level information *)
type level_info = {
  li_qty : int
  ; li_price : int
}

(* best bid and ask information *)
type best_bid_ask = {
  bid_info : level_info option
  ; ask_info : level_info option
}

(* Best bid/ask for all of the books *)
type books_info = {
  book1 : best_bid_ask
  ; book2 : best_bid_ask
  ; book3 : best_bid_ask
}

(* Order type *)
type order = {
  o_qty : int
  ; o_price : int
  ; o_time : int
  ; o_id : int
  ; o_side : side
  ; o_client_id : int
  ; o_inst : instrument
  ; o_is_implied : bool
}

(* Helper function to make order creation simpler *)
let make si qty price id inst clientid isimp time =
  {o_qty = qty ; o_price = price; o_id = id; o_side = si;
   o_client_id = clientid; o_inst = inst; o_is_implied = isimp;
   o_time = time }


(* outright order book *)
type book = {
  b_buys : order list
  ; b_sells : order list
}

let empty_book = { b_buys = []; b_sells = [] }

(* Individual leg *)
type leg = {
  leg_sec_idx : outright_id
  ; leg_mult : int
}

(* Strategy is composed of legs *)
type strategy = {
  time_created : int
  ; leg1 : leg
  ; leg2 : leg
  ; leg3 : leg
}

(* Helper function to make strategy creation smaller *)
let make_strat tcreated m1 m2 m3 = {
  time_created = tcreated
  ; leg1 = { leg_sec_idx = OUT1; leg_mult = m1 }
  ; leg2 = { leg_sec_idx = OUT2; leg_mult = m2 }
  ; leg3 = { leg_sec_idx = OUT3; leg_mult = m3 }
}

type implied_strat_ord = {
  max_strat : int option
  ; strat_price : int option
}

(* New order message *)
type new_ord_msg = {
  no_client_id : int
  ; no_inst_type : instrument
  ; no_qty : int
  ; no_side : side
  ; no_price : int
}

(* cancel order ID *)
type cancel_ord_msg = {
  co_client_id : int
  ; co_order_id : int
  ; co_instrument : instrument
  ; co_side : side
}

(* Inbound messages type *)
type inbound_msg =
  | NewOrder of new_ord_msg
  | CancelOrder of cancel_ord_msg
  | ImpliedUncross

(* Helper function for creating new order messages *)
let make_no_msg cid inst qty sd p =
 NewOrder {
  no_client_id = cid
  ; no_inst_type = inst
  ; no_qty = qty
  ; no_side = sd
  ; no_price = p
 }

(* ack message *)
type ack_msg = {
  ack_client_id : int
  ; ack_order_id : int
  ; ack_inst_type : instrument
  ; ack_qty : int
  ; ack_side : side
  ; ack_price : int
}

(* fill information *)
type fill = {
  fill_client_id : int
  ; fill_qty : int
  ; fill_price : int
  ; fill_order_id : int
  ; fill_order_done : bool
}

(* uncross result *)
type uncross_res = {
  uncrossed_book : book
  ; uncrossed_fills : fill list
  ; uncrossed_qty : int
}

(* outbound message type *)
type outbound_msg =
  | Ack of ack_msg
  | Fill of fill
  | UncrossResult of uncross_res
;;

(* The entire market - strategy definitions, order books, messages, etc. s*)
type market = {

  (* current time*)
  curr_time : int

  (* used for order ID counter *)
  ; last_ord_id : int

  (* two strategy definitions *)
  ; strat1    : strategy
  ; strat2    : strategy

  (* outright books *)
  ; out_book1 : book
  ; out_book2 : book
  ; out_book3 : book

  (* strategy books *)
  ; s_book1   : book
  ; s_book2   : book

  (* inbound and outbound message queues *)
  ; inbound_msgs  : inbound_msg list
  ; outbound_msgs : outbound_msg list

}
Out[1]:
type side = BUY | SELL
type outright_id = OUT1 | OUT2 | OUT3
type strategy_id = STRAT1 | STRAT2
type month = Mar | Jun | Sep | Dec
val contract_expiry : outright_id -> month = <fun>
val month_to_int : month -> int = <fun>
val month_comp : month -> month -> bool = <fun>
type instrument = Strategy of strategy_id | Outright of outright_id
type level_info = { li_qty : int; li_price : int; }
type best_bid_ask = {
  bid_info : level_info option;
  ask_info : level_info option;
}
type books_info = {
  book1 : best_bid_ask;
  book2 : best_bid_ask;
  book3 : best_bid_ask;
}
type order = {
  o_qty : int;
  o_price : int;
  o_time : int;
  o_id : int;
  o_side : side;
  o_client_id : int;
  o_inst : instrument;
  o_is_implied : bool;
}
val make :
  side -> int -> int -> int -> instrument -> int -> bool -> int -> order =
  <fun>
type book = { b_buys : order list; b_sells : order list; }
val empty_book : book = {b_buys = []; b_sells = []}
type leg = { leg_sec_idx : outright_id; leg_mult : int; }
type strategy = { time_created : int; leg1 : leg; leg2 : leg; leg3 : leg; }
val make_strat : int -> int -> int -> int -> strategy = <fun>
type implied_strat_ord = {
  max_strat : int option;
  strat_price : int option;
}
type new_ord_msg = {
  no_client_id : int;
  no_inst_type : instrument;
  no_qty : int;
  no_side : side;
  no_price : int;
}
type cancel_ord_msg = {
  co_client_id : int;
  co_order_id : int;
  co_instrument : instrument;
  co_side : side;
}
type inbound_msg =
    NewOrder of new_ord_msg
  | CancelOrder of cancel_ord_msg
  | ImpliedUncross
val make_no_msg : int -> instrument -> int -> side -> int -> inbound_msg =
  <fun>
type ack_msg = {
  ack_client_id : int;
  ack_order_id : int;
  ack_inst_type : instrument;
  ack_qty : int;
  ack_side : side;
  ack_price : int;
}
type fill = {
  fill_client_id : int;
  fill_qty : int;
  fill_price : int;
  fill_order_id : int;
  fill_order_done : bool;
}
type uncross_res = {
  uncrossed_book : book;
  uncrossed_fills : fill list;
  uncrossed_qty : int;
}
type outbound_msg =
    Ack of ack_msg
  | Fill of fill
  | UncrossResult of uncross_res
type market = {
  curr_time : int;
  last_ord_id : int;
  strat1 : strategy;
  strat2 : strategy;
  out_book1 : book;
  out_book2 : book;
  out_book3 : book;
  s_book1 : book;
  s_book2 : book;
  inbound_msgs : inbound_msg list;
  outbound_msgs : outbound_msg list;
}

1.2 Custom type printers

One of Imandra's powerful features is the ability to combine logic (pure subset of OCaml) and program (all of OCaml) modes. In the following cell, we will create and install a custom type printer (HTML) for an order book. So that next time a value of this type is computed within a cell, this printer would be used instead of the generic one.

In [2]:
(* Here's an example of a custom printer that we can install for arbitrary data types. *)

#program;;
#require "tyxml";;
let html_of_order (o : order) =
  let module H = Tyxml.Html in
  H.div
  ~a:(if o.o_is_implied then [H.a_style "color: red"] else [])
  [ H.div
    ~a:[H.a_style "font-size: 1.4em"]
    [H.txt (Format.asprintf "%s (%s)" (Z.to_string o.o_price) (Z.to_string o.o_qty))]
  ; H.div (if o.o_is_implied then [H.txt "Implied"] else [])
  ]

let doc_of_order (o:order) =
  let module H = Tyxml.Html in
  Document.html (H.div [html_of_order o]);;

#install_doc doc_of_order

let html_of_book ?(title="") (b: book) =
  let module H = Tyxml.Html in
  let rec build_rows acc buys sells =
      match buys, sells with
      | b :: bs, s :: ss -> build_rows (acc @ [H.tr [H.td [html_of_order b]; H.td [html_of_order s]]]) bs ss
      | b :: bs, [] -> build_rows (acc @ [H.tr [H.td [html_of_order b]; H.td [H.txt "-"]]]) bs []
      | [], s :: ss -> build_rows (acc @ [H.tr [H.td [H.txt "-"]; H.td [html_of_order s]]]) [] ss
      | [], [] -> acc
  in
  H.div
  ~a:[H.a_style "margin-right:1em; display: flex; flex-direction: column; align-items: center; justify-content: flex-start"]
  [ H.div ~a:[H.a_style "font-weight: bold"] [H.txt title]
  ; H.table
    ~thead:(H.thead [H.tr [H.th [H.txt "Buys"]; H.th [H.txt "Sells"]]])
    (build_rows [] b.b_buys b.b_sells)]

let doc_of_book (b:book) =
  let module H = Tyxml.Html in
  Document.html (H.div [html_of_book ~title:"M1 Mar21" b]);;

#install_doc doc_of_book;;

let html_of_market (m: market) =
  let module H = Tyxml.Html in
  H.div
  [ H.div ~a:[H.a_style "display: flex"]
    [ html_of_book ~title:"Strategy 1" m.s_book1
    ; html_of_book ~title:"Strategy 2" m.s_book2
    ]
  ; H.div ~a:[H.a_style "margin-top: 1em; display: flex"]
    [ html_of_book ~title:"Book 1" m.out_book1
    ; html_of_book ~title:"Book 2" m.out_book2
    ; html_of_book ~title:"Book 3" m.out_book3
    ]]

let doc_of_market (m : market) =
  let module H = Tyxml.Html in
  Document.html (html_of_market m);;

#install_doc doc_of_market;;

#logic;;
Out[2]:
/usr/local/var/imandra/_opam/lib/re: added to search path
/usr/local/var/imandra/_opam/lib/re/re.cma: loaded
/usr/local/var/imandra/_opam/lib/uchar: added to search path
/usr/local/var/imandra/_opam/lib/uutf: added to search path
/usr/local/var/imandra/_opam/lib/uutf/uutf.cma: loaded
/usr/local/var/imandra/_opam/lib/tyxml/functor: added to search path
/usr/local/var/imandra/_opam/lib/tyxml/functor/tyxml_f.cma: loaded
/usr/local/var/imandra/_opam/lib/tyxml: added to search path
/usr/local/var/imandra/_opam/lib/tyxml/tyxml.cma: loaded
- : unit = ()
val html_of_order : order -> [> Html_types.div ] Tyxml_html.elt = <fun>
File "jupyter cell 2", line 17, characters 16-41:
Error: This expression has type [> Html_types.div ] H.elt
       but an expression was expected of type Document.html
Line 2, characters 18-30:
2 |           let d = doc_of_order x in
                      ^^^^^^^^^^^^
Error: Unbound value doc_of_order
val html_of_book :
  ?title:string -> book -> [> Html_types.div ] Tyxml_html.elt = <fun>
File "jupyter cell 2", line 39, characters 16-58:
Error: This expression has type [> Html_types.div ] H.elt
       but an expression was expected of type Document.html
Line 2, characters 18-29:
2 |           let d = doc_of_book x in
                      ^^^^^^^^^^^
Error: Unbound value doc_of_book
val html_of_market : market -> [> Html_types.div ] Tyxml_html.elt = <fun>
File "jupyter cell 2", line 58, characters 16-34:
Error: This expression has type [> Html_types.div ] H.elt
       but an expression was expected of type Document.html
Line 2, characters 18-31:
2 |           let d = doc_of_market x in
                      ^^^^^^^^^^^^^
Error: Unbound value doc_of_market

1.3 Custom type printer example

In [3]:
let leg = { leg_sec_idx = OUT1; leg_mult = 1 } in

let strat = { time_created = 0; leg1 = leg; leg2 = leg; leg3 = leg } in

let b1 = {
  b_buys = [
    (make BUY 100 54 1 (Outright OUT1) 1 true 1)
    ;(make BUY 100 54 2 (Outright OUT1) 1 false 1)
  ]
  ; b_sells = [
    (make SELL 100 54 3 (Outright OUT1) 1 false 1)
    ;(make SELL 100 54 4 (Outright OUT1) 1 false 1)
  ] } in

  { curr_time = 1
  ; last_ord_id = 1
  ; strat1 = strat
  ; strat2 = strat
  ; out_book1 = b1
  ; out_book2 = b1
  ; out_book3 = b1
  ; s_book1 = b1
  ; s_book2 = b1
  ; inbound_msgs = []
  ; outbound_msgs = []
  }
Out[3]:
- : market =
{curr_time = 1; last_ord_id = 1;
 strat1 =
  {time_created = 0; leg1 = {leg_sec_idx = OUT1; leg_mult = 1};
   leg2 = {leg_sec_idx = OUT1; leg_mult = 1};
   leg3 = {leg_sec_idx = OUT1; leg_mult = 1}};
 strat2 =
  {time_created = 0; leg1 = {leg_sec_idx = OUT1; leg_mult = 1};
   leg2 = {leg_sec_idx = OUT1; leg_mult = 1};
   leg3 = {leg_sec_idx = OUT1; leg_mult = 1}};
 out_book1 =
  {b_buys =
    [{o_qty = 100; o_price = 54; o_time = 1; o_id = 1; o_side = BUY;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = true};
     {o_qty = 100; o_price = 54; o_time = 1; o_id = 2; o_side = BUY;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = false}];
   b_sells =
    [{o_qty = 100; o_price = 54; o_time = 1; o_id = 3; o_side = SELL;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = false};
     {o_qty = 100; o_price = 54; o_time = 1; o_id = 4; o_side = SELL;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = false}]};
 out_book2 =
  {b_buys =
    [{o_qty = 100; o_price = 54; o_time = 1; o_id = 1; o_side = BUY;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = true};
     {o_qty = 100; o_price = 54; o_time = 1; o_id = 2; o_side = BUY;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = false}];
   b_sells =
    [{o_qty = 100; o_price = 54; o_time = 1; o_id = 3; o_side = SELL;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = false};
     {o_qty = 100; o_price = 54; o_time = 1; o_id = 4; o_side = SELL;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = false}]};
 out_book3 =
  {b_buys =
    [{o_qty = 100; o_price = 54; o_time = 1; o_id = 1; o_side = BUY;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = true};
     {o_qty = 100; o_price = 54; o_time = 1; o_id = 2; o_side = BUY;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = false}];
   b_sells =
    [{o_qty = 100; o_price = 54; o_time = 1; o_id = 3; o_side = SELL;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = false};
     {o_qty = 100; o_price = 54; o_time = 1; o_id = 4; o_side = SELL;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = false}]};
 s_book1 =
  {b_buys =
    [{o_qty = 100; o_price = 54; o_time = 1; o_id = 1; o_side = BUY;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = true};
     {o_qty = 100; o_price = 54; o_time = 1; o_id = 2; o_side = BUY;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = false}];
   b_sells =
    [{o_qty = 100; o_price = 54; o_time = 1; o_id = 3; o_side = SELL;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = false};
     {o_qty = 100; o_price = 54; o_time = 1; o_id = 4; o_side = SELL;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = false}]};
 s_book2 =
  {b_buys =
    [{o_qty = 100; o_price = 54; o_time = 1; o_id = 1; o_side = BUY;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = true};
     {o_qty = 100; o_price = 54; o_time = 1; o_id = 2; o_side = BUY;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = false}];
   b_sells =
    [{o_qty = 100; o_price = 54; o_time = 1; o_id = 3; o_side = SELL;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = false};
     {o_qty = 100; o_price = 54; o_time = 1; o_id = 4; o_side = SELL;
      o_client_id = 1; o_inst = Outright OUT1; o_is_implied = false}]};
 inbound_msgs = []; outbound_msgs = []}

2. Outright uncrossing logic

2.1 Order book operatons (inserting, cancelling orders)

In [4]:
(* Convert fills into outbound messages *)
let rec create_fill_msgs (f : fill list) =
  match f with
  | [] -> []
  | x::xs -> (Fill x) :: create_fill_msgs xs

(* TODO: recode this with higher-order functions *)
let rec cancel_ord_side (orders : order list) (c : cancel_ord_msg) =
  match orders with
  | [] -> []
  | x::xs ->
    begin
      if (x.o_client_id = c.co_client_id) && (x.o_id = c.co_order_id) then xs
      else x :: (cancel_ord_side xs c)
    end

(* Helper to cancel orders *)
let cancel_ord_book (co : cancel_ord_msg) (b : book) =
  match co.co_side with
  | BUY -> { b with b_buys = (cancel_ord_side b.b_buys co) }
  | SELL -> { b with b_sells = (cancel_ord_side b.b_sells co) }

(* function used insert individual orders *)
let rec insert_order_side (orders : order list) (o : order) =
  match orders with
  | [] -> [ o ]
  | x::xs ->
    begin
      if o.o_side = BUY then
        (if o.o_price > x.o_price then o :: orders else x :: (insert_order_side xs o))
      else
        (if o.o_price < x.o_price then o :: orders else x :: (insert_order_side xs o))
    end

(* insert order into the book *)
let insert_order (o : order) (b : book) =
  if o.o_side = BUY then
    { b with b_buys = (insert_order_side b.b_buys o) }
  else
    { b with b_sells = (insert_order_side b.b_sells o) }

(* The fills are adjusted to a single fill price during the uncross *)
let rec adjust_fill_prices (fills : fill list) ( f_price : int ) =
  match fills with
  | [] -> []
  | x::xs -> { x with fill_price = f_price } :: ( adjust_fill_prices xs f_price )
;;
Out[4]:
val create_fill_msgs : fill list -> outbound_msg list = <fun>
val cancel_ord_side : order list -> cancel_ord_msg -> order list = <fun>
val cancel_ord_book : cancel_ord_msg -> book -> book = <fun>
val insert_order_side : order list -> order -> order list = <fun>
val insert_order : order -> book -> book = <fun>
val adjust_fill_prices : fill list -> int -> fill list = <fun>
termination proof

Termination proof

call `create_fill_msgs (List.tl f)` from `create_fill_msgs f`
originalcreate_fill_msgs f
subcreate_fill_msgs (List.tl f)
original ordinalOrdinal.Int (_cnt f)
sub ordinalOrdinal.Int (_cnt (List.tl f))
path[not Is_a([], f)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.022s
details
Expand
smt_stats
num checks8
arith-assume-eqs11
arith-make-feasible67
arith-max-columns50
arith-conflicts2
rlimit count3806
mk clause104
datatype occurs check42
mk bool var160
arith-lower37
datatype splits3
decisions54
propagations63
interface eqs11
arith-max-rows24
conflicts6
datatype accessor ax9
datatype constructor ax7
num allocs2395327
final checks17
added eqs114
del clause77
arith eq adapter35
arith-upper58
memory10.050000
max memory10.050000
Expand
  • start[0.022s]
      let (_x_0 : int) = count.list count.fill f in
      let (_x_1 : fill list) = List.tl f in
      let (_x_2 : int) = count.list count.fill _x_1 in
      not Is_a([], f) && _x_0 >= 0 && _x_2 >= 0
      ==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
  • simplify
    into
    let (_x_0 : fill list) = List.tl f in
    let (_x_1 : int) = count.list count.fill _x_0 in
    let (_x_2 : int) = count.list count.fill f in
    (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
    || not ((not Is_a([], f) && _x_2 >= 0) && _x_1 >= 0)
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|`count.list count.fill[0]`_1911| f_1900)
        expansions
        • unroll
          expr
          (|`count.list count.fill[0]`_1911| (|get.::.1_1884| f_1900))
          expansions
          • unroll
            expr
            (|Ordinal.<<_126| (|Ordinal.Int_111|
                                (|`count.list count.fill[0]`_1911| (|get.::…
            expansions
            • Unsat

            termination proof

            Termination proof

            call `cancel_ord_side (List.tl orders) c` from `cancel_ord_side orders c`
            originalcancel_ord_side orders c
            subcancel_ord_side (List.tl orders) c
            original ordinalOrdinal.Int (_cnt orders)
            sub ordinalOrdinal.Int (_cnt (List.tl orders))
            path[let (_x_0 : order) = List.hd orders in not (_x_0.o_client_id = c.co_client_id && _x_0.o_id = c.co_order_id) && not Is_a([], orders)]
            proof
            detailed proof
            ground_instances3
            definitions0
            inductions0
            search_time
            0.017s
            details
            Expand
            smt_stats
            num checks8
            arith-assume-eqs15
            arith-make-feasible81
            arith-max-columns59
            arith-conflicts2
            rlimit count5540
            mk clause130
            datatype occurs check71
            mk bool var339
            arith-lower45
            datatype splits51
            decisions102
            propagations75
            interface eqs15
            arith-max-rows29
            conflicts6
            datatype accessor ax34
            datatype constructor ax80
            num allocs5959081
            final checks21
            added eqs400
            del clause97
            arith eq adapter43
            arith-upper70
            memory10.460000
            max memory10.460000
            Expand
            • start[0.017s]
                let (_x_0 : order) = List.hd orders in
                let (_x_1 : int) = c.co_client_id in
                let (_x_2 : int) = c.co_order_id in
                let (_x_3 : int) = count.list count.order orders in
                let (_x_4 : order list) = List.tl orders in
                let (_x_5 : int) = count.list count.order _x_4 in
                let (_x_6 : order) = List.hd _x_4 in
                not (_x_0.o_client_id = _x_1 && _x_0.o_id = _x_2)
                && not Is_a([], orders) && _x_3 >= 0 && _x_5 >= 0
                ==> not
                    (not (_x_6.o_client_id = _x_1 && _x_6.o_id = _x_2)
                     && not Is_a([], _x_4))
                    || Ordinal.( << ) (Ordinal.Int _x_5) (Ordinal.Int _x_3)
            • simplify
              into
              let (_x_0 : order list) = List.tl orders in
              let (_x_1 : order) = List.hd _x_0 in
              let (_x_2 : int) = c.co_client_id in
              let (_x_3 : int) = c.co_order_id in
              let (_x_4 : int) = count.list count.order _x_0 in
              let (_x_5 : int) = count.list count.order orders in
              let (_x_6 : order) = List.hd orders in
              (not
               (not (_x_1.o_client_id = _x_2 && _x_1.o_id = _x_3) && not Is_a([], _x_0))
               || Ordinal.( << ) (Ordinal.Int _x_4) (Ordinal.Int _x_5))
              || not
                 (((not (_x_6.o_client_id = _x_2 && _x_6.o_id = _x_3)
                    && not Is_a([], orders))
                   && _x_5 >= 0)
                  && _x_4 >= 0)
              expansions
              []
              rewrite_steps
                forward_chaining
                • unroll
                  expr
                  (|`count.list count.order[0]`_1961| orders_1948)
                  expansions
                  • unroll
                    expr
                    (|`count.list count.order[0]`_1961| (|get.::.1_1946| orders_1948))
                    expansions
                    • unroll
                      expr
                      (|Ordinal.<<_126| (|Ordinal.Int_111|
                                          (|`count.list count.order[0]`_1961|
                             …
                      expansions
                      • Unsat

                      termination proof

                      Termination proof

                      call `insert_order_side (List.tl orders) o` from `insert_order_side orders o`
                      originalinsert_order_side orders o
                      subinsert_order_side (List.tl orders) o
                      original ordinalOrdinal.Int (_cnt orders)
                      sub ordinalOrdinal.Int (_cnt (List.tl orders))
                      path[not (o.o_price > (List.hd orders).o_price) && o.o_side = BUY && not Is_a([], orders)]
                      proof
                      detailed proof
                      ground_instances3
                      definitions0
                      inductions0
                      search_time
                      0.019s
                      details
                      Expand
                      smt_stats
                      num checks8
                      arith-assume-eqs13
                      arith-make-feasible79
                      arith-max-columns61
                      arith-conflicts2
                      rlimit count11263
                      mk clause124
                      datatype occurs check63
                      mk bool var348
                      arith-lower45
                      datatype splits59
                      decisions90
                      propagations76
                      interface eqs13
                      arith-max-rows30
                      conflicts6
                      datatype accessor ax36
                      datatype constructor ax78
                      num allocs12448066
                      final checks19
                      added eqs420
                      del clause91
                      arith eq adapter41
                      arith-upper68
                      memory16.640000
                      max memory16.640000
                      Expand
                      • start[0.019s]
                          let (_x_0 : int) = o.o_price in
                          let (_x_1 : bool) = o.o_side = BUY in
                          let (_x_2 : int) = count.list count.order orders in
                          let (_x_3 : order list) = List.tl orders in
                          let (_x_4 : int) = count.list count.order _x_3 in
                          let (_x_5 : int) = (List.hd _x_3).o_price in
                          let (_x_6 : bool) = not Is_a([], _x_3) in
                          not (_x_0 > (List.hd orders).o_price)
                          && _x_1 && not Is_a([], orders) && _x_2 >= 0 && _x_4 >= 0
                          ==> not (not (_x_0 > _x_5) && _x_1 && _x_6)
                              && not (not (_x_0 < _x_5) && not _x_1 && _x_6)
                              || Ordinal.( << ) (Ordinal.Int _x_4) (Ordinal.Int _x_2)
                      • simplify
                        into
                        let (_x_0 : order list) = List.tl orders in
                        let (_x_1 : int) = count.list count.order _x_0 in
                        let (_x_2 : int) = count.list count.order orders in
                        let (_x_3 : int) = o.o_price in
                        let (_x_4 : int) = (List.hd _x_0).o_price in
                        let (_x_5 : bool) = o.o_side = BUY in
                        let (_x_6 : bool) = not Is_a([], _x_0) in
                        (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                         || not ((_x_3 <= _x_4 && _x_5) && _x_6)
                            && not ((_x_4 <= _x_3 && not _x_5) && _x_6))
                        || not
                           ((((_x_3 <= (List.hd orders).o_price && _x_5) && not Is_a([], orders))
                             && _x_2 >= 0)
                            && _x_1 >= 0)
                        expansions
                        []
                        rewrite_steps
                          forward_chaining
                          • unroll
                            expr
                            (|`count.list count.order[0]`_2047| orders_2032)
                            expansions
                            • unroll
                              expr
                              (|`count.list count.order[0]`_2047| (|get.::.1_2031| orders_2032))
                              expansions
                              • unroll
                                expr
                                (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                    (|`count.list count.order[0]`_2047|
                                       …
                                expansions
                                • Unsat

                                call `insert_order_side (List.tl orders) o` from `insert_order_side orders o`
                                originalinsert_order_side orders o
                                subinsert_order_side (List.tl orders) o
                                original ordinalOrdinal.Int (_cnt orders)
                                sub ordinalOrdinal.Int (_cnt (List.tl orders))
                                path[not (o.o_price < (List.hd orders).o_price) && not (o.o_side = BUY) && not Is_a([], orders)]
                                proof
                                detailed proof
                                ground_instances3
                                definitions0
                                inductions0
                                search_time
                                0.024s
                                details
                                Expand
                                smt_stats
                                num checks8
                                arith-assume-eqs14
                                arith-make-feasible83
                                arith-max-columns62
                                arith-conflicts2
                                rlimit count5736
                                mk clause130
                                datatype occurs check67
                                mk bool var368
                                arith-lower46
                                datatype splits63
                                decisions95
                                propagations85
                                interface eqs14
                                arith-max-rows31
                                conflicts7
                                datatype accessor ax39
                                datatype constructor ax85
                                num allocs9126377
                                final checks20
                                added eqs444
                                del clause97
                                arith eq adapter44
                                arith-upper75
                                memory13.830000
                                max memory13.830000
                                Expand
                                • start[0.024s]
                                    let (_x_0 : int) = o.o_price in
                                    let (_x_1 : bool) = o.o_side = BUY in
                                    let (_x_2 : bool) = not _x_1 in
                                    let (_x_3 : int) = count.list count.order orders in
                                    let (_x_4 : order list) = List.tl orders in
                                    let (_x_5 : int) = count.list count.order _x_4 in
                                    let (_x_6 : int) = (List.hd _x_4).o_price in
                                    let (_x_7 : bool) = not Is_a([], _x_4) in
                                    not (_x_0 < (List.hd orders).o_price)
                                    && _x_2 && not Is_a([], orders) && _x_3 >= 0 && _x_5 >= 0
                                    ==> not (not (_x_0 > _x_6) && _x_1 && _x_7)
                                        && not (not (_x_0 < _x_6) && _x_2 && _x_7)
                                        || Ordinal.( << ) (Ordinal.Int _x_5) (Ordinal.Int _x_3)
                                • simplify
                                  into
                                  let (_x_0 : order list) = List.tl orders in
                                  let (_x_1 : int) = count.list count.order _x_0 in
                                  let (_x_2 : int) = count.list count.order orders in
                                  let (_x_3 : int) = o.o_price in
                                  let (_x_4 : int) = (List.hd _x_0).o_price in
                                  let (_x_5 : bool) = o.o_side = BUY in
                                  let (_x_6 : bool) = not Is_a([], _x_0) in
                                  let (_x_7 : bool) = not _x_5 in
                                  (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                   || not ((_x_3 <= _x_4 && _x_5) && _x_6)
                                      && not ((_x_4 <= _x_3 && _x_7) && _x_6))
                                  || not
                                     (((((List.hd orders).o_price <= _x_3 && _x_7) && not Is_a([], orders))
                                       && _x_2 >= 0)
                                      && _x_1 >= 0)
                                  expansions
                                  []
                                  rewrite_steps
                                    forward_chaining
                                    • unroll
                                      expr
                                      (|`count.list count.order[0]`_2047| orders_2032)
                                      expansions
                                      • unroll
                                        expr
                                        (|`count.list count.order[0]`_2047| (|get.::.1_2031| orders_2032))
                                        expansions
                                        • unroll
                                          expr
                                          (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                              (|`count.list count.order[0]`_2047|
                                                 …
                                          expansions
                                          • Unsat

                                          termination proof

                                          Termination proof

                                          call `adjust_fill_prices (List.tl fills) f_price` from `adjust_fill_prices fills f_price`
                                          originaladjust_fill_prices fills f_price
                                          subadjust_fill_prices (List.tl fills) f_price
                                          original ordinalOrdinal.Int (_cnt fills)
                                          sub ordinalOrdinal.Int (_cnt (List.tl fills))
                                          path[not Is_a([], fills)]
                                          proof
                                          detailed proof
                                          ground_instances3
                                          definitions0
                                          inductions0
                                          search_time
                                          0.016s
                                          details
                                          Expand
                                          smt_stats
                                          num checks8
                                          arith-assume-eqs12
                                          arith-make-feasible77
                                          arith-max-columns51
                                          arith-conflicts2
                                          rlimit count4061
                                          mk clause114
                                          datatype occurs check45
                                          mk bool var175
                                          arith-lower44
                                          datatype splits3
                                          decisions65
                                          propagations73
                                          interface eqs12
                                          arith-max-rows25
                                          conflicts8
                                          datatype accessor ax9
                                          datatype constructor ax7
                                          num allocs20681736
                                          final checks18
                                          added eqs131
                                          del clause87
                                          arith eq adapter42
                                          arith-upper68
                                          memory16.990000
                                          max memory16.990000
                                          Expand
                                          • start[0.016s]
                                              let (_x_0 : int) = count.list count.fill fills in
                                              let (_x_1 : fill list) = List.tl fills in
                                              let (_x_2 : int) = count.list count.fill _x_1 in
                                              not Is_a([], fills) && _x_0 >= 0 && _x_2 >= 0
                                              ==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                          • simplify
                                            into
                                            let (_x_0 : fill list) = List.tl fills in
                                            let (_x_1 : int) = count.list count.fill _x_0 in
                                            let (_x_2 : int) = count.list count.fill fills in
                                            (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                            || not ((not Is_a([], fills) && _x_2 >= 0) && _x_1 >= 0)
                                            expansions
                                            []
                                            rewrite_steps
                                              forward_chaining
                                              • unroll
                                                expr
                                                (|`count.list count.fill[0]`_2184| fills_2171)
                                                expansions
                                                • unroll
                                                  expr
                                                  (|`count.list count.fill[0]`_2184| (|get.::.1_2170| fills_2171))
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                        (|`count.list count.fill[0]`_2184|
                                                            …
                                                    expansions
                                                    • Unsat

                                                    2.2 Book uncross

                                                    In [5]:
                                                    (* Measure for proving termination of `uncross_book` below *)
                                                    let book_measure b =
                                                      Ordinal.of_int (List.length b.b_buys + List.length b.b_sells)
                                                    
                                                    let rec uncross_book (b : book) (fills : fill list) (filled_qty : int) =
                                                      match b.b_buys, b.b_sells with
                                                      | [], [] | _, [] | [], _ ->
                                                        (* we need to check whether there have been fills before,
                                                          if so we need to adjust fill prices before getting out *)
                                                        begin
                                                          match fills with
                                                          | [] -> { uncrossed_book = b; uncrossed_fills = fills; uncrossed_qty = filled_qty }
                                                          | x::xs ->
                                                            let fills' = x :: (adjust_fill_prices xs x.fill_price) in
                                                          { uncrossed_book = b; uncrossed_fills = fills'; uncrossed_qty = filled_qty }
                                                        end
                                                      | buy::bs, sell::ss ->
                                                        if buy.o_price >= sell.o_price then
                                                          begin
                                                            (* compute the fill qty and price *)
                                                            let fill_qty = if buy.o_qty < sell.o_qty then buy.o_qty else sell.o_qty in
                                                            let fill_price = (buy.o_price + sell.o_price) / 2 in
                                                    
                                                            (* update the orders that traded *)
                                                            let buy' = { buy with o_qty = buy.o_qty - fill_qty } in
                                                            let sell' = { sell with o_qty = sell.o_qty - fill_qty } in
                                                    
                                                            (* create the fills *)
                                                            let fill1 = {
                                                              fill_client_id = buy.o_client_id
                                                              ; fill_qty = fill_qty
                                                              ; fill_price = fill_price
                                                              ; fill_order_id = buy.o_id
                                                              ; fill_order_done = true } in
                                                    
                                                            let fill2 = {
                                                              fill_client_id = sell.o_client_id
                                                              ; fill_qty = fill_qty
                                                              ; fill_price = fill_price
                                                              ; fill_order_id = sell.o_id
                                                              ; fill_order_done = true } in
                                                    
                                                            (* now update the books and fills *)
                                                            let new_buys = if buy'.o_qty = 0 then bs else buy'::bs in
                                                            let new_sells = if sell'.o_qty = 0 then ss else sell'::ss in
                                                            let b' = {
                                                              b_buys = new_buys
                                                              ; b_sells = new_sells } in
                                                    
                                                            (* We should not be generating fills for implied orders - there's
                                                              a different mechanism for that *)
                                                            let fills' = if not buy.o_is_implied then
                                                              fill1 :: fills else fills in
                                                            let fills' = if not sell.o_is_implied then
                                                              fill2 :: fills' else fills' in
                                                    
                                                            (* recursively go to the next level *)
                                                            uncross_book b' fills' (filled_qty + fill_qty)
                                                          end
                                                    
                                                        else
                                                          (* nothing to do here *)
                                                          { uncrossed_book = b; uncrossed_fills = fills; uncrossed_qty = filled_qty }
                                                    [@@measure book_measure b]
                                                    ;;
                                                    
                                                    Out[5]:
                                                    val book_measure : book -> Ordinal.t = <fun>
                                                    val uncross_book : book -> fill list -> int -> uncross_res = <fun>
                                                    
                                                    termination proof

                                                    Termination proof

                                                    call `let (_x_0 : order list) = b.b_buys in let (_x_1 : order) = List.hd _x_0 in let (_x_2 : int) = _x_1.o_qty in let (_x_3 : order list) = b.b_sells in let (_x_4 : order) = List.hd _x_3 in let (_x_5 : int) = _x_4.o_qty in let (_x_6 : int) = if _x_2 < _x_5 then _x_2 else _x_5 in let (_x_7 : int) = _x_2 - _x_6 in let (_x_8 : order list) = List.tl _x_0 in let (_x_9 : int) = _x_5 - _x_6 in let (_x_10 : order list) = List.tl _x_3 in let (_x_11 : int) = (_x_1.o_price + _x_4.o_price) / 2 in let (_x_12 : fill list) = if not _x_1.o_is_implied then {fill_client_id = _x_1.o_client_id; fill_qty = _x_6; fill_price = _x_11; fill_order_id = _x_1.o_id; fill_order_done = true} :: fills else fills in uncross_book {b_buys = if _x_7 = 0 then _x_8 else {_x_1 with o_qty = _x_7} :: _x_8; b_sells = if _x_9 = 0 then _x_10 else {_x_4 with o_qty = _x_9} :: _x_10} (if not _x_4.o_is_implied then {fill_client_id = _x_4.o_client_id; fill_qty = _x_6; fill_price = _x_11; fill_order_id = _x_4.o_id; fill_order_done = true} :: _x_12 else _x_12) (filled_qty + _x_6)` from `uncross_book b fills filled_qty`
                                                    originaluncross_book b fills filled_qty
                                                    sublet (_x_0 : order list) = b.b_buys in let (_x_1 : order) = List.hd _x_0 in let (_x_2 : int) = _x_1.o_qty in let (_x_3 : order list) = b.b_sells in let (_x_4 : order) = List.hd _x_3 in let (_x_5 : int) = _x_4.o_qty in let (_x_6 : int) = if _x_2 < _x_5 then _x_2 else _x_5 in let (_x_7 : int) = _x_2 - _x_6 in let (_x_8 : order list) = List.tl _x_0 in let (_x_9 : int) = _x_5 - _x_6 in let (_x_10 : order list) = List.tl _x_3 in let (_x_11 : int) = (_x_1.o_price + _x_4.o_price) / 2 in let (_x_12 : fill list) = if not _x_1.o_is_implied then {fill_client_id = _x_1.o_client_id; fill_qty = _x_6; fill_price = _x_11; fill_order_id = _x_1.o_id; fill_order_done = true} :: fills else fills in uncross_book {b_buys = if _x_7 = 0 then _x_8 else {_x_1 with o_qty = _x_7} :: _x_8; b_sells = if _x_9 = 0 then _x_10 else {_x_4 with o_qty = _x_9} :: _x_10} (if not _x_4.o_is_implied then {fill_client_id = _x_4.o_client_id; fill_qty = _x_6; fill_price = _x_11; fill_order_id = _x_4.o_id; fill_order_done = true} :: _x_12 else _x_12) (filled_qty + _x_6)
                                                    original ordinalbook_measure b
                                                    sub ordinallet (_x_0 : order list) = b.b_buys in let (_x_1 : order) = List.hd _x_0 in let (_x_2 : int) = _x_1.o_qty in let (_x_3 : order list) = b.b_sells in let (_x_4 : order) = List.hd _x_3 in let (_x_5 : int) = _x_4.o_qty in let (_x_6 : int) = if _x_2 < _x_5 then _x_2 else _x_5 in let (_x_7 : int) = _x_2 - _x_6 in let (_x_8 : order list) = List.tl _x_0 in let (_x_9 : int) = _x_5 - _x_6 in let (_x_10 : order list) = List.tl _x_3 in book_measure {b_buys = if _x_7 = 0 then _x_8 else {_x_1 with o_qty = _x_7} :: _x_8; b_sells = if _x_9 = 0 then _x_10 else {_x_4 with o_qty = _x_9} :: _x_10}
                                                    path[(List.hd b.b_buys).o_price >= (List.hd b.b_sells).o_price && not Is_a([], b.b_buys) && not Is_a([], b.b_sells)]
                                                    proof
                                                    detailed proof
                                                    ground_instances5
                                                    definitions0
                                                    inductions0
                                                    search_time
                                                    0.024s
                                                    details
                                                    Expand
                                                    smt_stats
                                                    num checks12
                                                    arith-assume-eqs6
                                                    arith-make-feasible81
                                                    arith-max-columns40
                                                    arith-conflicts4
                                                    rlimit count10199
                                                    arith-cheap-eqs34
                                                    mk clause125
                                                    datatype occurs check95
                                                    mk bool var701
                                                    arith-lower53
                                                    arith-diseq18
                                                    datatype splits148
                                                    decisions175
                                                    arith-propagations8
                                                    propagations150
                                                    interface eqs4
                                                    arith-bound-propagations-cheap8
                                                    arith-max-rows19
                                                    conflicts21
                                                    datatype accessor ax90
                                                    minimized lits1
                                                    arith-bound-propagations-lp6
                                                    datatype constructor ax257
                                                    num allocs26488768
                                                    final checks17
                                                    added eqs1266
                                                    del clause75
                                                    arith eq adapter61
                                                    arith-upper76
                                                    time0.001000
                                                    memory20.420000
                                                    max memory20.420000
                                                    Expand
                                                    • start[0.024s]
                                                        let (_x_0 : order list) = b.b_buys in
                                                        let (_x_1 : order) = List.hd _x_0 in
                                                        let (_x_2 : int) = _x_1.o_price in
                                                        let (_x_3 : order list) = b.b_sells in
                                                        let (_x_4 : order) = List.hd _x_3 in
                                                        let (_x_5 : int) = _x_4.o_price in
                                                        let (_x_6 : int) = List.length _x_0 + List.length _x_3 in
                                                        let (_x_7 : int) = if _x_6 >= 0 then _x_6 else 0 in
                                                        let (_x_8 : int) = List.length ….b_buys + List.length ….b_sells in
                                                        let (_x_9 : int) = if _x_8 >= 0 then _x_8 else 0 in
                                                        let (_x_10 : int) = _x_1.o_qty in
                                                        let (_x_11 : int) = _x_4.o_qty in
                                                        let (_x_12 : int) = if _x_10 < _x_11 then _x_10 else _x_11 in
                                                        let (_x_13 : int) = _x_10 - _x_12 in
                                                        let (_x_14 : order list) = List.tl _x_0 in
                                                        let (_x_15 : order list)
                                                            = if _x_13 = 0 then _x_14
                                                              else
                                                                {o_qty = _x_13; o_price = _x_2; o_time = …; o_id = …;
                                                                 o_side = …; o_client_id = …; o_inst = …; o_is_implied = …}
                                                                :: _x_14
                                                        in
                                                        let (_x_16 : int) = _x_11 - _x_12 in
                                                        let (_x_17 : order list) = List.tl _x_3 in
                                                        let (_x_18 : order list)
                                                            = if _x_16 = 0 then _x_17
                                                              else
                                                                {o_qty = _x_16; o_price = _x_5; o_time = …; o_id = …;
                                                                 o_side = …; o_client_id = …; o_inst = …; o_is_implied = …}
                                                                :: _x_17
                                                        in
                                                        _x_2 >= _x_5
                                                        && not Is_a([], _x_0) && not Is_a([], _x_3) && _x_7 >= 0 && _x_9 >= 0
                                                        ==> not
                                                            ((List.hd _x_15).o_price >= (List.hd _x_18).o_price
                                                             && not Is_a([], _x_15) && not Is_a([], _x_18))
                                                            || Ordinal.( << ) (Ordinal.Int _x_9) (Ordinal.Int _x_7)
                                                    • simplify
                                                      into
                                                      let (_x_0 : order list) = b.b_buys in
                                                      let (_x_1 : order) = List.hd _x_0 in
                                                      let (_x_2 : int) = _x_1.o_qty in
                                                      let (_x_3 : order list) = b.b_sells in
                                                      let (_x_4 : order) = List.hd _x_3 in
                                                      let (_x_5 : int) = _x_4.o_qty in
                                                      let (_x_6 : int) = -1 * (if _x_5 <= _x_2 then _x_5 else _x_2) in
                                                      let (_x_7 : int) = _x_2 + _x_6 in
                                                      let (_x_8 : int) = _x_1.o_price in
                                                      let (_x_9 : order list) = List.tl _x_0 in
                                                      let (_x_10 : order list)
                                                          = if _x_7 = 0 then _x_9
                                                            else
                                                              {o_qty = _x_7; o_price = _x_8; o_time = …; o_id = …;
                                                               o_side = …; o_client_id = …; o_inst = …; o_is_implied = …}
                                                              :: _x_9
                                                      in
                                                      let (_x_11 : int) = _x_5 + _x_6 in
                                                      let (_x_12 : int) = _x_4.o_price in
                                                      let (_x_13 : order list) = List.tl _x_3 in
                                                      let (_x_14 : order list)
                                                          = if _x_11 = 0 then _x_13
                                                            else
                                                              {o_qty = _x_11; o_price = _x_12; o_time = …; o_id = …;
                                                               o_side = …; o_client_id = …; o_inst = …; o_is_implied = …}
                                                              :: _x_13
                                                      in
                                                      let (_x_15 : int) = List.length _x_10 + List.length _x_14 in
                                                      let (_x_16 : int) = List.length _x_0 + List.length _x_3 in
                                                      (not
                                                       (((List.hd _x_10).o_price >= (List.hd _x_14).o_price && not Is_a([], _x_10))
                                                        && not Is_a([], _x_14))
                                                       || Ordinal.( << ) (Ordinal.Int (if _x_15 >= 0 then _x_15 else 0))
                                                          (Ordinal.Int (if _x_16 >= 0 then _x_16 else 0)))
                                                      || not ((_x_8 >= _x_12 && not Is_a([], _x_0)) && not Is_a([], _x_3))
                                                      expansions
                                                      []
                                                      rewrite_steps
                                                        forward_chaining
                                                        • unroll
                                                          expr
                                                          (|List.length_2240| (b_sells_89 b_2252))
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (|List.length_2240| (b_buys_88 b_2252))
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (let ((a!1 (<= (o_qty_68 (|get.::.0_2234| (b_sells_89 b_2252)))
                                                                             (o_qty_68 (|get.::.0_…
                                                              expansions
                                                              • unroll
                                                                expr
                                                                (let ((a!1 (<= (o_qty_68 (|get.::.0_2234| (b_sells_89 b_2252)))
                                                                               (o_qty_68 (|get.::.0_…
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (let ((a!1 (<= (o_qty_68 (|get.::.0_2234| (b_sells_89 b_2252)))
                                                                                 (o_qty_68 (|get.::.0_…
                                                                  expansions
                                                                  • Unsat

                                                                  We now have a function that does something real - uncross_book (b : book) (fills : fill list) (filled_qty : int). Let's experiment how it works with some concrete values.

                                                                  In [6]:
                                                                  let book1 = {
                                                                    b_buys = [
                                                                      (make BUY 100 55 1 (Outright OUT1) 1 false 1)
                                                                      ; (make BUY 100 50 2 (Outright OUT1) 1 false 1)
                                                                      ]
                                                                   ; b_sells = [
                                                                      (make BUY 100 54 3 (Outright OUT1) 1 false 1)
                                                                      ; (make BUY 100 54 4 (Outright OUT1) 1 false 1)
                                                                    ]
                                                                  } in
                                                                  
                                                                  uncross_book book1 [] 0
                                                                  
                                                                  Out[6]:
                                                                  - : uncross_res =
                                                                  {uncrossed_book =
                                                                    {b_buys =
                                                                      [{o_qty = 100; o_price = 50; o_time = 1; o_id = 2; o_side = BUY;
                                                                        o_client_id = 1; o_inst = Outright OUT1; o_is_implied = false}];
                                                                     b_sells =
                                                                      [{o_qty = 100; o_price = 54; o_time = 1; o_id = 4; o_side = BUY;
                                                                        o_client_id = 1; o_inst = Outright OUT1; o_is_implied = false}]};
                                                                   uncrossed_fills =
                                                                    [{fill_client_id = 1; fill_qty = 100; fill_price = 54; fill_order_id = 3;
                                                                      fill_order_done = true};
                                                                     {fill_client_id = 1; fill_qty = 100; fill_price = 54; fill_order_id = 1;
                                                                      fill_order_done = true}];
                                                                   uncrossed_qty = 100}
                                                                  

                                                                  2.3 A few verification goals

                                                                  Let's try to verify some verification goals.

                                                                  The first one will make sure that for an order book that is sorted (so the best bid/ask orders will be the first ones in their respective lists. Note: this is not based on the 'imbalance' of the order book, this is simply taking the midpointt of the most aggressive orders.

                                                                  In [7]:
                                                                  (* Returns true if the orders are sorted with respect to price *)
                                                                  let rec side_price_sorted (si : side) (orders : order list) =
                                                                    match orders with
                                                                    | [] -> true
                                                                    | x::[] -> true
                                                                    | x::y::xs ->
                                                                      if si = BUY then
                                                                        begin
                                                                          if y.o_price > x.o_price && x.o_price > 0 then false else (side_price_sorted si (y::xs))
                                                                        end
                                                                      else
                                                                        begin
                                                                          if y.o_price < x.o_price && y.o_price > 0 then false else (side_price_sorted si (y::xs))
                                                                        end
                                                                  ;;
                                                                  
                                                                  (* Let's make sure all the fills have this price *)
                                                                  let rec fills_good_price (fills : fill list) (p : int) =
                                                                    match fills with
                                                                    | [] -> true
                                                                    | x::xs -> (x.fill_price = p) && (fills_good_price xs p)
                                                                  ;;
                                                                  
                                                                  (** Let's to verify some properties *)
                                                                  let fill_price_midpoint (b : book) =
                                                                  
                                                                    let buys_sorted = side_price_sorted BUY b.b_buys in
                                                                    let sells_sorted = side_price_sorted SELL b.b_sells in
                                                                  
                                                                    let result_good =
                                                                      begin
                                                                        match b.b_buys, b.b_sells with
                                                                        | [], _ -> true
                                                                        | _, [] -> true
                                                                        | x::xs, y::ys ->
                                                                          let unc_res = uncross_book b [] 0 in
                                                                          if x.o_price >= y.o_price then
                                                                            let midprice = (x.o_price + y.o_price) / 2 in
                                                                            (List.length unc_res.uncrossed_fills) > 0 && (fills_good_price unc_res.uncrossed_fills midprice)
                                                                          else
                                                                            true
                                                                      end in
                                                                  
                                                                    (* This is the 'punchline'... if the sides are price-sorted, then the fills will be the first midpoint *)
                                                                    (buys_sorted && sells_sorted) ==> result_good
                                                                  ;;
                                                                  
                                                                  
                                                                  verify fill_price_midpoint
                                                                  
                                                                  Out[7]:
                                                                  val side_price_sorted : side -> order list -> bool = <fun>
                                                                  val fills_good_price : fill list -> int -> bool = <fun>
                                                                  val fill_price_midpoint : book -> bool = <fun>
                                                                  - : book -> bool = <fun>
                                                                  module CX : sig val b : book end
                                                                  
                                                                  termination proof

                                                                  Termination proof

                                                                  call `let (_x_0 : order list) = List.tl orders in side_price_sorted si ((List.hd _x_0) :: (List.tl _x_0))` from `side_price_sorted si orders`
                                                                  originalside_price_sorted si orders
                                                                  sublet (_x_0 : order list) = List.tl orders in side_price_sorted si ((List.hd _x_0) :: (List.tl _x_0))
                                                                  original ordinalOrdinal.Int (_cnt orders)
                                                                  sub ordinallet (_x_0 : order list) = List.tl orders in Ordinal.Int (_cnt ((List.hd _x_0) :: (List.tl _x_0)))
                                                                  path[let (_x_0 : int) = (List.hd orders).o_price in not ((List.hd (List.tl orders)).o_price > _x_0 && _x_0 > 0) && si = BUY && not Is_a([], List.tl orders) && not Is_a([], orders)]
                                                                  proof
                                                                  detailed proof
                                                                  ground_instances3
                                                                  definitions0
                                                                  inductions0
                                                                  search_time
                                                                  0.019s
                                                                  details
                                                                  Expand
                                                                  smt_stats
                                                                  num checks8
                                                                  arith-assume-eqs15
                                                                  arith-make-feasible94
                                                                  arith-max-columns67
                                                                  arith-conflicts2
                                                                  rlimit count13306
                                                                  mk clause144
                                                                  datatype occurs check54
                                                                  mk bool var373
                                                                  arith-lower56
                                                                  datatype splits52
                                                                  decisions109
                                                                  propagations98
                                                                  interface eqs15
                                                                  arith-max-rows34
                                                                  conflicts6
                                                                  datatype accessor ax33
                                                                  arith-bound-propagations-lp3
                                                                  datatype constructor ax83
                                                                  num allocs45975839
                                                                  final checks21
                                                                  added eqs443
                                                                  del clause105
                                                                  arith eq adapter50
                                                                  arith-upper85
                                                                  memory23.780000
                                                                  max memory23.780000
                                                                  Expand
                                                                  • start[0.019s]
                                                                      let (_x_0 : order list) = List.tl orders in
                                                                      let (_x_1 : order) = List.hd _x_0 in
                                                                      let (_x_2 : int) = _x_1.o_price in
                                                                      let (_x_3 : int) = (List.hd orders).o_price in
                                                                      let (_x_4 : bool) = si = BUY in
                                                                      let (_x_5 : int) = count.list count.order orders in
                                                                      let (_x_6 : int) = count.list count.order (_x_1 :: …) in
                                                                      let (_x_7 : int) = (List.hd …).o_price in
                                                                      let (_x_8 : bool) = not Is_a([], …) in
                                                                      not (_x_2 > _x_3 && _x_3 > 0)
                                                                      && _x_4
                                                                         && not Is_a([], _x_0) && not Is_a([], orders) && _x_5 >= 0 && _x_6 >= 0
                                                                      ==> not (not (_x_7 > _x_2 && _x_2 > 0) && _x_4 && _x_8)
                                                                          && not (not (_x_7 < _x_2 && _x_7 > 0) && not _x_4 && _x_8)
                                                                          || Ordinal.( << ) (Ordinal.Int _x_6) (Ordinal.Int _x_5)
                                                                  • simplify
                                                                    into
                                                                    let (_x_0 : order list) = List.tl orders in
                                                                    let (_x_1 : order) = List.hd _x_0 in
                                                                    let (_x_2 : int) = count.list count.order (_x_1 :: …) in
                                                                    let (_x_3 : int) = count.list count.order orders in
                                                                    let (_x_4 : int) = (List.hd …).o_price in
                                                                    let (_x_5 : int) = _x_1.o_price in
                                                                    let (_x_6 : bool) = si = BUY in
                                                                    let (_x_7 : bool) = not Is_a([], …) in
                                                                    let (_x_8 : int) = (List.hd orders).o_price in
                                                                    (Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_3)
                                                                     || not ((not (not (_x_4 <= _x_5) && not (_x_5 <= 0)) && _x_6) && _x_7)
                                                                        && not
                                                                           ((not (not (_x_5 <= _x_4) && not (_x_4 <= 0)) && not _x_6) && _x_7))
                                                                    || not
                                                                       (((((not (not (_x_5 <= _x_8) && not (_x_8 <= 0)) && _x_6)
                                                                           && not Is_a([], _x_0))
                                                                          && not Is_a([], orders))
                                                                         && _x_3 >= 0)
                                                                        && _x_2 >= 0)
                                                                    expansions
                                                                    []
                                                                    rewrite_steps
                                                                      forward_chaining
                                                                      • unroll
                                                                        expr
                                                                        (|`count.list count.order[0]`_2479| orders_2465)
                                                                        expansions
                                                                        • unroll
                                                                          expr
                                                                          (|`count.list count.order[0]`_2479|
                                                                            (|::_3| (|get.::.0_2462| (|get.::.1_2463| orders_2465))
                                                                                …
                                                                          expansions
                                                                          • unroll
                                                                            expr
                                                                            (let ((a!1 (|`count.list count.order[0]`_2479|
                                                                                         (|::_3| (|get.::.0_2462| (|get.::.1_2463…
                                                                            expansions
                                                                            • Unsat

                                                                            call `let (_x_0 : order list) = List.tl orders in side_price_sorted si ((List.hd _x_0) :: (List.tl _x_0))` from `side_price_sorted si orders`
                                                                            originalside_price_sorted si orders
                                                                            sublet (_x_0 : order list) = List.tl orders in side_price_sorted si ((List.hd _x_0) :: (List.tl _x_0))
                                                                            original ordinalOrdinal.Int (_cnt orders)
                                                                            sub ordinallet (_x_0 : order list) = List.tl orders in Ordinal.Int (_cnt ((List.hd _x_0) :: (List.tl _x_0)))
                                                                            path[let (_x_0 : int) = (List.hd (List.tl orders)).o_price in not (_x_0 < (List.hd orders).o_price && _x_0 > 0) && not (si = BUY) && not Is_a([], List.tl orders) && not Is_a([], orders)]
                                                                            proof
                                                                            detailed proof
                                                                            ground_instances3
                                                                            definitions0
                                                                            inductions0
                                                                            search_time
                                                                            0.024s
                                                                            details
                                                                            Expand
                                                                            smt_stats
                                                                            num checks8
                                                                            arith-assume-eqs12
                                                                            arith-make-feasible99
                                                                            arith-max-columns64
                                                                            arith-conflicts2
                                                                            rlimit count6722
                                                                            arith-cheap-eqs53
                                                                            mk clause133
                                                                            datatype occurs check59
                                                                            mk bool var380
                                                                            arith-lower59
                                                                            datatype splits56
                                                                            decisions119
                                                                            propagations93
                                                                            interface eqs12
                                                                            arith-max-rows31
                                                                            conflicts7
                                                                            datatype accessor ax36
                                                                            arith-bound-propagations-lp1
                                                                            datatype constructor ax89
                                                                            num allocs38825551
                                                                            final checks18
                                                                            added eqs452
                                                                            del clause97
                                                                            arith eq adapter49
                                                                            arith-upper84
                                                                            memory20.870000
                                                                            max memory20.870000
                                                                            Expand
                                                                            • start[0.024s]
                                                                                let (_x_0 : order list) = List.tl orders in
                                                                                let (_x_1 : order) = List.hd _x_0 in
                                                                                let (_x_2 : int) = _x_1.o_price in
                                                                                let (_x_3 : bool) = _x_2 > 0 in
                                                                                let (_x_4 : bool) = si = BUY in
                                                                                let (_x_5 : bool) = not _x_4 in
                                                                                let (_x_6 : int) = count.list count.order orders in
                                                                                let (_x_7 : int) = count.list count.order (_x_1 :: …) in
                                                                                let (_x_8 : int) = (List.hd …).o_price in
                                                                                let (_x_9 : bool) = not Is_a([], …) in
                                                                                not (_x_2 < (List.hd orders).o_price && _x_3)
                                                                                && _x_5
                                                                                   && not Is_a([], _x_0) && not Is_a([], orders) && _x_6 >= 0 && _x_7 >= 0
                                                                                ==> not (not (_x_8 > _x_2 && _x_3) && _x_4 && _x_9)
                                                                                    && not (not (_x_8 < _x_2 && _x_8 > 0) && _x_5 && _x_9)
                                                                                    || Ordinal.( << ) (Ordinal.Int _x_7) (Ordinal.Int _x_6)
                                                                            • simplify
                                                                              into
                                                                              let (_x_0 : order list) = List.tl orders in
                                                                              let (_x_1 : order) = List.hd _x_0 in
                                                                              let (_x_2 : int) = count.list count.order (_x_1 :: …) in
                                                                              let (_x_3 : int) = count.list count.order orders in
                                                                              let (_x_4 : int) = (List.hd …).o_price in
                                                                              let (_x_5 : int) = _x_1.o_price in
                                                                              let (_x_6 : bool) = not (_x_5 <= 0) in
                                                                              let (_x_7 : bool) = si = BUY in
                                                                              let (_x_8 : bool) = not Is_a([], …) in
                                                                              let (_x_9 : bool) = not _x_7 in
                                                                              (Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_3)
                                                                               || not ((not (not (_x_4 <= _x_5) && _x_6) && _x_7) && _x_8)
                                                                                  && not ((not (not (_x_5 <= _x_4) && not (_x_4 <= 0)) && _x_9) && _x_8))
                                                                              || not
                                                                                 (((((not (not ((List.hd orders).o_price <= _x_5) && _x_6) && _x_9)
                                                                                     && not Is_a([], _x_0))
                                                                                    && not Is_a([], orders))
                                                                                   && _x_3 >= 0)
                                                                                  && _x_2 >= 0)
                                                                              expansions
                                                                              []
                                                                              rewrite_steps
                                                                                forward_chaining
                                                                                • unroll
                                                                                  expr
                                                                                  (|`count.list count.order[0]`_2479| orders_2465)
                                                                                  expansions
                                                                                  • unroll
                                                                                    expr
                                                                                    (|`count.list count.order[0]`_2479|
                                                                                      (|::_3| (|get.::.0_2462| (|get.::.1_2463| orders_2465))
                                                                                          …
                                                                                    expansions
                                                                                    • unroll
                                                                                      expr
                                                                                      (let ((a!1 (|`count.list count.order[0]`_2479|
                                                                                                   (|::_3| (|get.::.0_2462| (|get.::.1_2463…
                                                                                      expansions
                                                                                      • Unsat

                                                                                      termination proof

                                                                                      Termination proof

                                                                                      call `fills_good_price (List.tl fills) p` from `fills_good_price fills p`
                                                                                      originalfills_good_price fills p
                                                                                      subfills_good_price (List.tl fills) p
                                                                                      original ordinalOrdinal.Int (_cnt fills)
                                                                                      sub ordinalOrdinal.Int (_cnt (List.tl fills))
                                                                                      path[(List.hd fills).fill_price = p && not Is_a([], fills)]
                                                                                      proof
                                                                                      detailed proof
                                                                                      ground_instances3
                                                                                      definitions0
                                                                                      inductions0
                                                                                      search_time
                                                                                      0.021s
                                                                                      details
                                                                                      Expand
                                                                                      smt_stats
                                                                                      num checks8
                                                                                      arith-assume-eqs7
                                                                                      arith-make-feasible60
                                                                                      arith-max-columns43
                                                                                      arith-conflicts2
                                                                                      rlimit count3837
                                                                                      mk clause89
                                                                                      datatype occurs check27
                                                                                      mk bool var153
                                                                                      arith-lower36
                                                                                      datatype splits3
                                                                                      decisions48
                                                                                      propagations67
                                                                                      interface eqs7
                                                                                      arith-max-rows19
                                                                                      conflicts8
                                                                                      datatype accessor ax9
                                                                                      datatype constructor ax7
                                                                                      num allocs60767310
                                                                                      final checks13
                                                                                      added eqs116
                                                                                      del clause64
                                                                                      arith eq adapter34
                                                                                      arith-upper57
                                                                                      memory23.870000
                                                                                      max memory23.870000
                                                                                      Expand
                                                                                      • start[0.021s]
                                                                                          let (_x_0 : int) = count.list count.fill fills in
                                                                                          let (_x_1 : fill list) = List.tl fills in
                                                                                          let (_x_2 : int) = count.list count.fill _x_1 in
                                                                                          (List.hd fills).fill_price = p
                                                                                          && not Is_a([], fills) && _x_0 >= 0 && _x_2 >= 0
                                                                                          ==> not ((List.hd _x_1).fill_price = p && not Is_a([], _x_1))
                                                                                              || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                      • simplify
                                                                                        into
                                                                                        let (_x_0 : fill list) = List.tl fills in
                                                                                        let (_x_1 : int) = count.list count.fill _x_0 in
                                                                                        let (_x_2 : int) = count.list count.fill fills in
                                                                                        (not ((List.hd _x_0).fill_price = p && not Is_a([], _x_0))
                                                                                         || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                                        || not
                                                                                           ((((List.hd fills).fill_price = p && not Is_a([], fills)) && _x_2 >= 0)
                                                                                            && _x_1 >= 0)
                                                                                        expansions
                                                                                        []
                                                                                        rewrite_steps
                                                                                          forward_chaining
                                                                                          • unroll
                                                                                            expr
                                                                                            (|`count.list count.fill[0]`_2645| fills_2632)
                                                                                            expansions
                                                                                            • unroll
                                                                                              expr
                                                                                              (|`count.list count.fill[0]`_2645| (|get.::.1_2631| fills_2632))
                                                                                              expansions
                                                                                              • unroll
                                                                                                expr
                                                                                                (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                    (|`count.list count.fill[0]`_2645|
                                                                                                        …
                                                                                                expansions
                                                                                                • Unsat

                                                                                                Counterexample (after 6 steps, 0.031s):
                                                                                                 let (b : book) =
                                                                                                  {b_buys =
                                                                                                    [{o_qty = 10450; o_price = (-6864); o_time = 21; o_id = 10; o_side = BUY;
                                                                                                      o_client_id = 11; o_inst = (Strategy (STRAT1)); o_is_implied = true}];
                                                                                                   b_sells =
                                                                                                    [{o_qty = (-1); o_price = (-23594); o_time = 3; o_id = 4; o_side = BUY;
                                                                                                      o_client_id = 5; o_inst = (Strategy (STRAT1)); o_is_implied = true}]}
                                                                                                
                                                                                                Refuted
                                                                                                proof attempt
                                                                                                ground_instances6
                                                                                                definitions0
                                                                                                inductions0
                                                                                                search_time
                                                                                                0.031s
                                                                                                details
                                                                                                Expand
                                                                                                smt_stats
                                                                                                num checks13
                                                                                                arith-assume-eqs23
                                                                                                arith-make-feasible94
                                                                                                arith-max-columns48
                                                                                                rlimit count15720
                                                                                                arith-gcd-calls2
                                                                                                arith-cheap-eqs75
                                                                                                mk clause279
                                                                                                datatype occurs check276
                                                                                                mk bool var1171
                                                                                                arith-lower82
                                                                                                arith-diseq17
                                                                                                datatype splits242
                                                                                                decisions339
                                                                                                arith-propagations10
                                                                                                arith-patches-success2
                                                                                                propagations281
                                                                                                arith-patches2
                                                                                                interface eqs23
                                                                                                arith-bound-propagations-cheap10
                                                                                                arith-max-rows24
                                                                                                conflicts13
                                                                                                datatype accessor ax150
                                                                                                minimized lits2
                                                                                                arith-bound-propagations-lp3
                                                                                                datatype constructor ax412
                                                                                                num allocs78859707
                                                                                                final checks38
                                                                                                added eqs2105
                                                                                                del clause123
                                                                                                arith eq adapter67
                                                                                                arith-upper72
                                                                                                time0.004000
                                                                                                memory24.870000
                                                                                                max memory24.870000
                                                                                                Expand
                                                                                                • start[0.031s]
                                                                                                    let (_x_0 : order list) = ( :var_0: ).b_buys in
                                                                                                    let (_x_1 : order list) = ( :var_0: ).b_sells in
                                                                                                    side_price_sorted BUY _x_0 && side_price_sorted SELL _x_1
                                                                                                    ==> (if Is_a([], _x_0) then true
                                                                                                         else
                                                                                                         if Is_a([], _x_1) then true
                                                                                                         else
                                                                                                         if (List.hd _x_0).o_price >= (List.hd _x_1).o_price
                                                                                                         then List.length … > 0 && fills_good_price … … else true)
                                                                                                • simplify

                                                                                                  into
                                                                                                  let (_x_0 : order list) = ( :var_0: ).b_sells in
                                                                                                  let (_x_1 : order list) = ( :var_0: ).b_buys in
                                                                                                  (((Is_a([], _x_0) || Is_a([], _x_1))
                                                                                                    || not (List.length … <= 0) && fills_good_price … …)
                                                                                                   || not ((List.hd _x_1).o_price >= (List.hd _x_0).o_price))
                                                                                                  || not (side_price_sorted BUY _x_1 && side_price_sorted SELL _x_0)
                                                                                                  expansions
                                                                                                  []
                                                                                                  rewrite_steps
                                                                                                    forward_chaining
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (side_price_sorted_289 SELL_16 (b_sells_89 b_332))
                                                                                                      expansions
                                                                                                      • unroll
                                                                                                        expr
                                                                                                        (side_price_sorted_289 BUY_15 (b_buys_88 b_332))
                                                                                                        expansions
                                                                                                        • unroll
                                                                                                          expr
                                                                                                          (let ((a!1 (+ (o_price_69 (|get.::.0_2696| (b_buys_88 b_332)))
                                                                                                                        (o_price_69 (|get.::.0_…
                                                                                                          expansions
                                                                                                          • unroll
                                                                                                            expr
                                                                                                            (uncross_book_225 b_332 |[]_2| 0)
                                                                                                            expansions
                                                                                                            • unroll
                                                                                                              expr
                                                                                                              (|List.length_2703| (uncrossed_fills_163 (uncross_book_225 b_332 |[]_2| 0)))
                                                                                                              expansions
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (let ((a!1 (<= (o_qty_68 (|get.::.0_2696| (b_sells_89 b_332)))
                                                                                                                               (o_qty_68 (|get.::.0_2…
                                                                                                                expansions
                                                                                                                • Sat (Some let (b : book) = {b_buys = [{o_qty = 10450; o_price = (-6864); o_time = 21; o_id = 10; o_side = BUY; o_client_id = 11; o_inst = (Strategy (STRAT1)); o_is_implied = true}]; b_sells = [{o_qty = (-1); o_price = (-23594); o_time = 3; o_id = 4; o_side = BUY; o_client_id = 5; o_inst = (Strategy (STRAT1)); o_is_implied = true}]} )

                                                                                                                Our second verification goal will look to make sure that no quantities are lost during uncrossing. Note that no fills are generated for implied orders (there's a different mechanism for that), so when we look at the book we will only consider outright orders. Note that o_qty represents the residual order quantity - for this demo, we do not differentiate between original, filled and residual order quantity. When order is created, the qty is set to that number and is decreased when filled.

                                                                                                                In [8]:
                                                                                                                (* All no quantities get lost during uncross *)
                                                                                                                let no_lost_qtys (b : book) =
                                                                                                                
                                                                                                                  let rec qtys_pos_nonimp = function
                                                                                                                    | [] -> true
                                                                                                                    | x::xs -> x.o_qty >= 0 && not x.o_is_implied && (qtys_pos_nonimp xs) in
                                                                                                                
                                                                                                                  let rec sum_qtys = function
                                                                                                                    | [] -> 0
                                                                                                                    | x::xs -> x.o_qty + (sum_qtys xs) in
                                                                                                                
                                                                                                                  let rec sum_fill_qtys = function
                                                                                                                    | [] -> 0
                                                                                                                    | x::xs -> x.fill_qty + (sum_fill_qtys xs) in
                                                                                                                
                                                                                                                  let unc_res = uncross_book b [] 0 in
                                                                                                                
                                                                                                                  (* We need to make sure the book is non-negative *)
                                                                                                                  let book_nonneg_nonimp = (qtys_pos_nonimp b.b_buys) && (qtys_pos_nonimp b.b_sells) in
                                                                                                                
                                                                                                                  (* Let's sum up all of the quantities of orders before the uncross *)
                                                                                                                  let count_before = (sum_qtys b.b_buys) + (sum_qtys b.b_sells) in
                                                                                                                
                                                                                                                  (* And after *)
                                                                                                                  let count_after = (sum_qtys unc_res.uncrossed_book.b_buys) +
                                                                                                                                    (sum_qtys unc_res.uncrossed_book.b_sells) +
                                                                                                                                    (sum_fill_qtys unc_res.uncrossed_fills) in
                                                                                                                
                                                                                                                  book_nonneg_nonimp ==> (count_before = count_after)
                                                                                                                ;;
                                                                                                                
                                                                                                                verify ~upto:15 no_lost_qtys
                                                                                                                
                                                                                                                Out[8]:
                                                                                                                val no_lost_qtys : book -> bool = <fun>
                                                                                                                - : book -> bool = <fun>
                                                                                                                
                                                                                                                termination proof

                                                                                                                Termination proof

                                                                                                                call `recfun.no_lost_qtys.sum_fill_qtys.2 (List.tl _x)` from `recfun.no_lost_qtys.sum_fill_qtys.2 _x`
                                                                                                                originalrecfun.no_lost_qtys.sum_fill_qtys.2 _x
                                                                                                                subrecfun.no_lost_qtys.sum_fill_qtys.2 (List.tl _x)
                                                                                                                original ordinalOrdinal.Int (_cnt _x)
                                                                                                                sub ordinalOrdinal.Int (_cnt (List.tl _x))
                                                                                                                path[not Is_a([], _x)]
                                                                                                                proof
                                                                                                                detailed proof
                                                                                                                ground_instances3
                                                                                                                definitions0
                                                                                                                inductions0
                                                                                                                search_time
                                                                                                                0.017s
                                                                                                                details
                                                                                                                Expand
                                                                                                                smt_stats
                                                                                                                num checks8
                                                                                                                arith-assume-eqs12
                                                                                                                arith-make-feasible77
                                                                                                                arith-max-columns51
                                                                                                                arith-conflicts2
                                                                                                                rlimit count4061
                                                                                                                mk clause114
                                                                                                                datatype occurs check45
                                                                                                                mk bool var175
                                                                                                                arith-lower44
                                                                                                                datatype splits3
                                                                                                                decisions65
                                                                                                                propagations73
                                                                                                                interface eqs12
                                                                                                                arith-max-rows25
                                                                                                                conflicts8
                                                                                                                datatype accessor ax9
                                                                                                                datatype constructor ax7
                                                                                                                num allocs89074606
                                                                                                                final checks18
                                                                                                                added eqs131
                                                                                                                del clause87
                                                                                                                arith eq adapter42
                                                                                                                arith-upper68
                                                                                                                memory27.900000
                                                                                                                max memory27.900000
                                                                                                                Expand
                                                                                                                • start[0.017s]
                                                                                                                    let (_x_0 : int) = count.list count.fill _x in
                                                                                                                    let (_x_1 : fill list) = List.tl _x in
                                                                                                                    let (_x_2 : int) = count.list count.fill _x_1 in
                                                                                                                    not Is_a([], _x) && _x_0 >= 0 && _x_2 >= 0
                                                                                                                    ==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                • simplify
                                                                                                                  into
                                                                                                                  let (_x_0 : fill list) = List.tl _x in
                                                                                                                  let (_x_1 : int) = count.list count.fill _x_0 in
                                                                                                                  let (_x_2 : int) = count.list count.fill _x in
                                                                                                                  (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                                                                  || not ((not Is_a([], _x) && _x_2 >= 0) && _x_1 >= 0)
                                                                                                                  expansions
                                                                                                                  []
                                                                                                                  rewrite_steps
                                                                                                                    forward_chaining
                                                                                                                    • unroll
                                                                                                                      expr
                                                                                                                      (|`count.list count.fill[0]`_2861| _x_2850)
                                                                                                                      expansions
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (|`count.list count.fill[0]`_2861| (|get.::.1_2847| _x_2850))
                                                                                                                        expansions
                                                                                                                        • unroll
                                                                                                                          expr
                                                                                                                          (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                                              (|`count.list count.fill[0]`_2861|
                                                                                                                                  …
                                                                                                                          expansions
                                                                                                                          • Unsat

                                                                                                                          termination proof

                                                                                                                          Termination proof

                                                                                                                          call `recfun.no_lost_qtys.sum_qtys.1 (List.tl _x)` from `recfun.no_lost_qtys.sum_qtys.1 _x`
                                                                                                                          originalrecfun.no_lost_qtys.sum_qtys.1 _x
                                                                                                                          subrecfun.no_lost_qtys.sum_qtys.1 (List.tl _x)
                                                                                                                          original ordinalOrdinal.Int (_cnt _x)
                                                                                                                          sub ordinalOrdinal.Int (_cnt (List.tl _x))
                                                                                                                          path[not Is_a([], _x)]
                                                                                                                          proof
                                                                                                                          detailed proof
                                                                                                                          ground_instances3
                                                                                                                          definitions0
                                                                                                                          inductions0
                                                                                                                          search_time
                                                                                                                          0.015s
                                                                                                                          details
                                                                                                                          Expand
                                                                                                                          smt_stats
                                                                                                                          num checks8
                                                                                                                          arith-assume-eqs5
                                                                                                                          arith-make-feasible35
                                                                                                                          arith-max-columns39
                                                                                                                          arith-conflicts2
                                                                                                                          rlimit count8037
                                                                                                                          mk clause71
                                                                                                                          datatype occurs check48
                                                                                                                          mk bool var230
                                                                                                                          arith-lower17
                                                                                                                          datatype splits39
                                                                                                                          decisions46
                                                                                                                          propagations32
                                                                                                                          interface eqs5
                                                                                                                          arith-max-rows16
                                                                                                                          conflicts6
                                                                                                                          datatype accessor ax29
                                                                                                                          datatype constructor ax57
                                                                                                                          num allocs107234899
                                                                                                                          final checks11
                                                                                                                          added eqs261
                                                                                                                          del clause40
                                                                                                                          arith eq adapter16
                                                                                                                          arith-upper27
                                                                                                                          memory27.940000
                                                                                                                          max memory27.940000
                                                                                                                          Expand
                                                                                                                          • start[0.015s]
                                                                                                                              let (_x_0 : int) = count.list count.order _x in
                                                                                                                              let (_x_1 : order list) = List.tl _x in
                                                                                                                              let (_x_2 : int) = count.list count.order _x_1 in
                                                                                                                              not Is_a([], _x) && _x_0 >= 0 && _x_2 >= 0
                                                                                                                              ==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                          • simplify
                                                                                                                            into
                                                                                                                            let (_x_0 : int) = count.list count.order _x in
                                                                                                                            let (_x_1 : order list) = List.tl _x in
                                                                                                                            let (_x_2 : int) = count.list count.order _x_1 in
                                                                                                                            (not ((not Is_a([], _x) && _x_0 >= 0) && _x_2 >= 0) || Is_a([], _x_1))
                                                                                                                            || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                            expansions
                                                                                                                            []
                                                                                                                            rewrite_steps
                                                                                                                              forward_chaining
                                                                                                                              • unroll
                                                                                                                                expr
                                                                                                                                (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                                                    (|`count.list count.order[0]`_2897|
                                                                                                                                       …
                                                                                                                                expansions
                                                                                                                                • unroll
                                                                                                                                  expr
                                                                                                                                  (|`count.list count.order[0]`_2897| (|get.::.1_2843| _x_2890))
                                                                                                                                  expansions
                                                                                                                                  • unroll
                                                                                                                                    expr
                                                                                                                                    (|`count.list count.order[0]`_2897| _x_2890)
                                                                                                                                    expansions
                                                                                                                                    • Unsat

                                                                                                                                    termination proof

                                                                                                                                    Termination proof

                                                                                                                                    call `recfun.no_lost_qtys.qtys_pos_nonimp.0 (List.tl _x)` from `recfun.no_lost_qtys.qtys_pos_nonimp.0 _x`
                                                                                                                                    originalrecfun.no_lost_qtys.qtys_pos_nonimp.0 _x
                                                                                                                                    subrecfun.no_lost_qtys.qtys_pos_nonimp.0 (List.tl _x)
                                                                                                                                    original ordinalOrdinal.Int (_cnt _x)
                                                                                                                                    sub ordinalOrdinal.Int (_cnt (List.tl _x))
                                                                                                                                    path[not (List.hd _x).o_is_implied && (List.hd _x).o_qty >= 0 && not Is_a([], _x)]
                                                                                                                                    proof
                                                                                                                                    detailed proof
                                                                                                                                    ground_instances3
                                                                                                                                    definitions0
                                                                                                                                    inductions0
                                                                                                                                    search_time
                                                                                                                                    0.026s
                                                                                                                                    details
                                                                                                                                    Expand
                                                                                                                                    smt_stats
                                                                                                                                    num checks8
                                                                                                                                    arith-assume-eqs12
                                                                                                                                    arith-make-feasible77
                                                                                                                                    arith-max-columns54
                                                                                                                                    arith-conflicts2
                                                                                                                                    rlimit count12862
                                                                                                                                    mk clause110
                                                                                                                                    datatype occurs check98
                                                                                                                                    mk bool var277
                                                                                                                                    arith-lower41
                                                                                                                                    datatype splits39
                                                                                                                                    decisions71
                                                                                                                                    propagations65
                                                                                                                                    interface eqs12
                                                                                                                                    arith-max-rows25
                                                                                                                                    conflicts6
                                                                                                                                    datatype accessor ax29
                                                                                                                                    datatype constructor ax57
                                                                                                                                    num allocs126998635
                                                                                                                                    final checks18
                                                                                                                                    added eqs296
                                                                                                                                    del clause87
                                                                                                                                    arith eq adapter40
                                                                                                                                    arith-upper70
                                                                                                                                    memory28.060000
                                                                                                                                    max memory28.060000
                                                                                                                                    Expand
                                                                                                                                    • start[0.026s]
                                                                                                                                        let (_x_0 : order) = List.hd _x in
                                                                                                                                        let (_x_1 : int) = count.list count.order _x in
                                                                                                                                        let (_x_2 : order list) = List.tl _x in
                                                                                                                                        let (_x_3 : int) = count.list count.order _x_2 in
                                                                                                                                        let (_x_4 : order) = List.hd _x_2 in
                                                                                                                                        not _x_0.o_is_implied
                                                                                                                                        && _x_0.o_qty >= 0 && not Is_a([], _x) && _x_1 >= 0 && _x_3 >= 0
                                                                                                                                        ==> not (not _x_4.o_is_implied && _x_4.o_qty >= 0 && not Is_a([], _x_2))
                                                                                                                                            || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_1)
                                                                                                                                    • simplify
                                                                                                                                      into
                                                                                                                                      let (_x_0 : order list) = List.tl _x in
                                                                                                                                      let (_x_1 : int) = count.list count.order _x_0 in
                                                                                                                                      let (_x_2 : int) = count.list count.order _x in
                                                                                                                                      let (_x_3 : order) = List.hd _x_0 in
                                                                                                                                      let (_x_4 : order) = List.hd _x in
                                                                                                                                      (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                                                                                       || not ((not _x_3.o_is_implied && _x_3.o_qty >= 0) && not Is_a([], _x_0)))
                                                                                                                                      || not
                                                                                                                                         ((((not _x_4.o_is_implied && _x_4.o_qty >= 0) && not Is_a([], _x))
                                                                                                                                           && _x_2 >= 0)
                                                                                                                                          && _x_1 >= 0)
                                                                                                                                      expansions
                                                                                                                                      []
                                                                                                                                      rewrite_steps
                                                                                                                                        forward_chaining
                                                                                                                                        • unroll
                                                                                                                                          expr
                                                                                                                                          (|`count.list count.order[0]`_2897| _x_2926)
                                                                                                                                          expansions
                                                                                                                                          • unroll
                                                                                                                                            expr
                                                                                                                                            (|`count.list count.order[0]`_2897| (|get.::.1_2843| _x_2926))
                                                                                                                                            expansions
                                                                                                                                            • unroll
                                                                                                                                              expr
                                                                                                                                              (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                                                                  (|`count.list count.order[0]`_2897|
                                                                                                                                                     …
                                                                                                                                              expansions
                                                                                                                                              • Unsat

                                                                                                                                              Proved up to 15 steps

                                                                                                                                              2.4 Test generation

                                                                                                                                              First, we will decompose the function and then generate test cases for it.

                                                                                                                                              In [9]:
                                                                                                                                              (* This is a 'side_condition' function that tells decomposition that we're only interested in cases where the
                                                                                                                                              initial fills are empty *)
                                                                                                                                              let cond (b : book) (fills : fill list) (filled_qty : int) =
                                                                                                                                               fills = [] && filled_qty = 0
                                                                                                                                              ;;
                                                                                                                                              
                                                                                                                                              let d = Modular_decomp.top ~assuming:"cond" "uncross_book" ~prune:true [@@program];;
                                                                                                                                              
                                                                                                                                              Out[9]:
                                                                                                                                              val cond : book -> fill list -> int -> bool = <fun>
                                                                                                                                              val d : Modular_decomposition.t =
                                                                                                                                                {Imandra_interactive.Modular_decomp.MD.md_session = 1i;
                                                                                                                                                 md_f =
                                                                                                                                                  {Imandra_surface.Uid.name = "uncross_book"; id = <abstr>;
                                                                                                                                                   special_tag = <abstr>; namespace = <abstr>;
                                                                                                                                                   chash = Some mE5Q46wPGG4H9SmS1ZuNd4hfIpT5QRZwSC1omfx0zwU;
                                                                                                                                                   depth = (3i, 6i)};
                                                                                                                                                 md_args = [(b : book);(fills : fill list);(filled_qty : int)];
                                                                                                                                                 md_regions = <abstr>}
                                                                                                                                              
                                                                                                                                              Regions details

                                                                                                                                              No group selected.

                                                                                                                                              • Concrete regions are numbered
                                                                                                                                              • Unnumbered regions are groups whose children share a particular constraint
                                                                                                                                              • Click on a region to view its details
                                                                                                                                              • Double click on a region to zoom in on it
                                                                                                                                              • Shift+double click to zoom out
                                                                                                                                              • Hit escape to reset back to the top
                                                                                                                                              decomp of (uncross_book b, fills, filled_qty
                                                                                                                                              Reg_idConstraintsInvariant
                                                                                                                                              19
                                                                                                                                              • fills = []
                                                                                                                                              • filled_qty = 0
                                                                                                                                              • Is_a([], fills)
                                                                                                                                              • Is_a([], b.b_buys)
                                                                                                                                              • Is_a([], b.b_sells)
                                                                                                                                              {uncrossed_book = b; uncrossed_fills = fills; uncrossed_qty = filled_qty}
                                                                                                                                              18
                                                                                                                                              • fills = []
                                                                                                                                              • filled_qty = 0
                                                                                                                                              • Is_a([], fills)
                                                                                                                                              • not Is_a([], b.b_buys)
                                                                                                                                              • Is_a([], b.b_sells)
                                                                                                                                              {uncrossed_book = b; uncrossed_fills = fills; uncrossed_qty = filled_qty}
                                                                                                                                              17
                                                                                                                                              • fills = []
                                                                                                                                              • filled_qty = 0
                                                                                                                                              • Is_a([], fills)
                                                                                                                                              • Is_a([], b.b_buys)
                                                                                                                                              • not Is_a([], b.b_sells)
                                                                                                                                              {uncrossed_book = b; uncrossed_fills = fills; uncrossed_qty = filled_qty}
                                                                                                                                              12
                                                                                                                                              • fills = []
                                                                                                                                              • filled_qty = 0
                                                                                                                                              • not (List.hd b.b_buys).o_is_implied
                                                                                                                                              • not (List.hd b.b_sells).o_is_implied
                                                                                                                                              • not ((List.hd b.b_sells).o_qty - (List.hd b.b_buys).o_qty = 0)
                                                                                                                                              • (List.hd b.b_buys).o_qty < (List.hd b.b_sells).o_qty
                                                                                                                                              • (List.hd b.b_buys).o_price >= (List.hd b.b_sells).o_price
                                                                                                                                              • not Is_a([], b.b_buys)
                                                                                                                                              • not Is_a([], b.b_sells)
                                                                                                                                              let (_x_0 : order list) = b.b_buys in
                                                                                                                                              let (_x_1 : order list) = b.b_sells in
                                                                                                                                              let (_x_2 : order) = List.hd _x_1 in
                                                                                                                                              let (_x_3 : order) = List.hd _x_0 in
                                                                                                                                              let (_x_4 : int) = _x_3.o_qty in
                                                                                                                                              let (_x_5 : int) = (_x_3.o_price + _x_2.o_price) / 2 in
                                                                                                                                              uncross_book
                                                                                                                                              {b_buys = List.tl _x_0;
                                                                                                                                               b_sells = {_x_2 with o_qty = _x_2.o_qty - _x_4} :: (List.tl _x_1)}
                                                                                                                                              ({fill_client_id = _x_2.o_client_id; fill_qty = _x_4; fill_price = _x_5;
                                                                                                                                                fill_order_id = _x_2.o_id; fill_order_done = true}
                                                                                                                                               ::
                                                                                                                                               ({fill_client_id = _x_3.o_client_id; fill_qty = _x_4; fill_price = _x_5;
                                                                                                                                                 fill_order_id = _x_3.o_id; fill_order_done = true}
                                                                                                                                                :: fills))
                                                                                                                                              (filled_qty + _x_4)
                                                                                                                                              11
                                                                                                                                              • fills = []
                                                                                                                                              • filled_qty = 0
                                                                                                                                              • (List.hd b.b_buys).o_is_implied
                                                                                                                                              • not (List.hd b.b_sells).o_is_implied
                                                                                                                                              • not ((List.hd b.b_sells).o_qty - (List.hd b.b_buys).o_qty = 0)
                                                                                                                                              • (List.hd b.b_buys).o_qty < (List.hd b.b_sells).o_qty
                                                                                                                                              • (List.hd b.b_buys).o_price >= (List.hd b.b_sells).o_price
                                                                                                                                              • not Is_a([], b.b_buys)
                                                                                                                                              • not Is_a([], b.b_sells)
                                                                                                                                              let (_x_0 : order list) = b.b_buys in
                                                                                                                                              let (_x_1 : order list) = b.b_sells in
                                                                                                                                              let (_x_2 : order) = List.hd _x_1 in
                                                                                                                                              let (_x_3 : order) = List.hd _x_0 in
                                                                                                                                              let (_x_4 : int) = _x_3.o_qty in
                                                                                                                                              uncross_book
                                                                                                                                              {b_buys = List.tl _x_0;
                                                                                                                                               b_sells = {_x_2 with o_qty = _x_2.o_qty - _x_4} :: (List.tl _x_1)}
                                                                                                                                              ({fill_client_id = _x_2.o_client_id; fill_qty = _x_4;
                                                                                                                                                fill_price = (_x_3.o_price + _x_2.o_price) / 2; fill_order_id = _x_2.o_id;
                                                                                                                                                fill_order_done = true}
                                                                                                                                               :: fills)
                                                                                                                                              (filled_qty + _x_4)
                                                                                                                                              10
                                                                                                                                              • fills = []
                                                                                                                                              • filled_qty = 0
                                                                                                                                              • not (List.hd b.b_buys).o_is_implied
                                                                                                                                              • (List.hd b.b_sells).o_is_implied
                                                                                                                                              • not ((List.hd b.b_sells).o_qty - (List.hd b.b_buys).o_qty = 0)
                                                                                                                                              • (List.hd b.b_buys).o_qty < (List.hd b.b_sells).o_qty
                                                                                                                                              • (List.hd b.b_buys).o_price >= (List.hd b.b_sells).o_price
                                                                                                                                              • not Is_a([], b.b_buys)
                                                                                                                                              • not Is_a([], b.b_sells)
                                                                                                                                              let (_x_0 : order list) = b.b_buys in
                                                                                                                                              let (_x_1 : order list) = b.b_sells in
                                                                                                                                              let (_x_2 : order) = List.hd _x_1 in
                                                                                                                                              let (_x_3 : order) = List.hd _x_0 in
                                                                                                                                              let (_x_4 : int) = _x_3.o_qty in
                                                                                                                                              uncross_book
                                                                                                                                              {b_buys = List.tl _x_0;
                                                                                                                                               b_sells = {_x_2 with o_qty = _x_2.o_qty - _x_4} :: (List.tl _x_1)}
                                                                                                                                              ({fill_client_id = _x_3.o_client_id; fill_qty = _x_4;
                                                                                                                                                fill_price = (_x_3.o_price + _x_2.o_price) / 2; fill_order_id = _x_3.o_id;
                                                                                                                                                fill_order_done = true}
                                                                                                                                               :: fills)
                                                                                                                                              (filled_qty + _x_4)
                                                                                                                                              9
                                                                                                                                              • fills = []
                                                                                                                                              • filled_qty = 0
                                                                                                                                              • (List.hd b.b_buys).o_is_implied
                                                                                                                                              • (List.hd b.b_sells).o_is_implied
                                                                                                                                              • not ((List.hd b.b_sells).o_qty - (List.hd b.b_buys).o_qty = 0)
                                                                                                                                              • (List.hd b.b_buys).o_qty < (List.hd b.b_sells).o_qty
                                                                                                                                              • (List.hd b.b_buys).o_price >= (List.hd b.b_sells).o_price
                                                                                                                                              • not Is_a([], b.b_buys)
                                                                                                                                              • not Is_a([], b.b_sells)
                                                                                                                                              let (_x_0 : order list) = b.b_buys in
                                                                                                                                              let (_x_1 : order list) = b.b_sells in
                                                                                                                                              let (_x_2 : order) = List.hd _x_1 in
                                                                                                                                              let (_x_3 : int) = (List.hd _x_0).o_qty in
                                                                                                                                              uncross_book
                                                                                                                                              {b_buys = List.tl _x_0;
                                                                                                                                               b_sells = {_x_2 with o_qty = _x_2.o_qty - _x_3} :: (List.tl _x_1)}
                                                                                                                                              fills (filled_qty + _x_3)
                                                                                                                                              8
                                                                                                                                              • fills = []
                                                                                                                                              • filled_qty = 0
                                                                                                                                              • not (List.hd b.b_buys).o_is_implied
                                                                                                                                              • not (List.hd b.b_sells).o_is_implied
                                                                                                                                              • (List.hd b.b_buys).o_qty - (List.hd b.b_sells).o_qty = 0
                                                                                                                                              • not ((List.hd b.b_buys).o_qty < (List.hd b.b_sells).o_qty)
                                                                                                                                              • (List.hd b.b_buys).o_price >= (List.hd b.b_sells).o_price
                                                                                                                                              • not Is_a([], b.b_buys)
                                                                                                                                              • not Is_a([], b.b_sells)
                                                                                                                                              let (_x_0 : order list) = b.b_buys in
                                                                                                                                              let (_x_1 : order list) = b.b_sells in
                                                                                                                                              let (_x_2 : order) = List.hd _x_1 in
                                                                                                                                              let (_x_3 : int) = _x_2.o_qty in
                                                                                                                                              let (_x_4 : order) = List.hd _x_0 in
                                                                                                                                              let (_x_5 : int) = (_x_4.o_price + _x_2.o_price) / 2 in
                                                                                                                                              uncross_book {b_buys = List.tl _x_0; b_sells = List.tl _x_1}
                                                                                                                                              ({fill_client_id = _x_2.o_client_id; fill_qty = _x_3; fill_price = _x_5;
                                                                                                                                                fill_order_id = _x_2.o_id; fill_order_done = true}
                                                                                                                                               ::
                                                                                                                                               ({fill_client_id = _x_4.o_client_id; fill_qty = _x_3; fill_price = _x_5;
                                                                                                                                                 fill_order_id = _x_4.o_id; fill_order_done = true}
                                                                                                                                                :: fills))
                                                                                                                                              (filled_qty + _x_3)
                                                                                                                                              7
                                                                                                                                              • fills = []
                                                                                                                                              • filled_qty = 0
                                                                                                                                              • (List.hd b.b_buys).o_is_implied
                                                                                                                                              • not (List.hd b.b_sells).o_is_implied
                                                                                                                                              • (List.hd b.b_buys).o_qty - (List.hd b.b_sells).o_qty = 0
                                                                                                                                              • not ((List.hd b.b_buys).o_qty < (List.hd b.b_sells).o_qty)
                                                                                                                                              • (List.hd b.b_buys).o_price >= (List.hd b.b_sells).o_price
                                                                                                                                              • not Is_a([], b.b_buys)
                                                                                                                                              • not Is_a([], b.b_sells)
                                                                                                                                              let (_x_0 : order list) = b.b_buys in
                                                                                                                                              let (_x_1 : order list) = b.b_sells in
                                                                                                                                              let (_x_2 : order) = List.hd _x_1 in
                                                                                                                                              let (_x_3 : int) = _x_2.o_qty in
                                                                                                                                              uncross_book {b_buys = List.tl _x_0; b_sells = List.tl _x_1}
                                                                                                                                              ({fill_client_id = _x_2.o_client_id; fill_qty = _x_3;
                                                                                                                                                fill_price = ((List.hd _x_0).o_price + _x_2.o_price) / 2;
                                                                                                                                                fill_order_id = _x_2.o_id; fill_order_done = true}
                                                                                                                                               :: fills)
                                                                                                                                              (filled_qty + _x_3)
                                                                                                                                              6
                                                                                                                                              • fills = []
                                                                                                                                              • filled_qty = 0
                                                                                                                                              • not (List.hd b.b_buys).o_is_implied
                                                                                                                                              • (List.hd b.b_sells).o_is_implied
                                                                                                                                              • (List.hd b.b_buys).o_qty - (List.hd b.b_sells).o_qty = 0
                                                                                                                                              • not ((List.hd b.b_buys).o_qty < (List.hd b.b_sells).o_qty)
                                                                                                                                              • (List.hd b.b_buys).o_price >= (List.hd b.b_sells).o_price
                                                                                                                                              • not Is_a([], b.b_buys)
                                                                                                                                              • not Is_a([], b.b_sells)
                                                                                                                                              let (_x_0 : order list) = b.b_buys in
                                                                                                                                              let (_x_1 : order list) = b.b_sells in
                                                                                                                                              let (_x_2 : order) = List.hd _x_0 in
                                                                                                                                              let (_x_3 : order) = List.hd _x_1 in
                                                                                                                                              let (_x_4 : int) = _x_3.o_qty in
                                                                                                                                              uncross_book {b_buys = List.tl _x_0; b_sells = List.tl _x_1}
                                                                                                                                              ({fill_client_id = _x_2.o_client_id; fill_qty = _x_4;
                                                                                                                                                fill_price = (_x_2.o_price + _x_3.o_price) / 2; fill_order_id = _x_2.o_id;
                                                                                                                                                fill_order_done = true}
                                                                                                                                               :: fills)
                                                                                                                                              (filled_qty + _x_4)
                                                                                                                                              5
                                                                                                                                              • fills = []
                                                                                                                                              • filled_qty = 0
                                                                                                                                              • (List.hd b.b_buys).o_is_implied
                                                                                                                                              • (List.hd b.b_sells).o_is_implied
                                                                                                                                              • (List.hd b.b_buys).o_qty - (List.hd b.b_sells).o_qty = 0
                                                                                                                                              • not ((List.hd b.b_buys).o_qty < (List.hd b.b_sells).o_qty)
                                                                                                                                              • (List.hd b.b_buys).o_price >= (List.hd b.b_sells).o_price
                                                                                                                                              • not Is_a([], b.b_buys)
                                                                                                                                              • not Is_a([], b.b_sells)
                                                                                                                                              let (_x_0 : order list) = b.b_sells in
                                                                                                                                              uncross_book {b_buys = List.tl b.b_buys; b_sells = List.tl _x_0} fills
                                                                                                                                              (filled_qty + (List.hd _x_0).o_qty)
                                                                                                                                              4
                                                                                                                                              • fills = []
                                                                                                                                              • filled_qty = 0
                                                                                                                                              • not (List.hd b.b_buys).o_is_implied
                                                                                                                                              • not (List.hd b.b_sells).o_is_implied
                                                                                                                                              • not ((List.hd b.b_buys).o_qty - (List.hd b.b_sells).o_qty = 0)
                                                                                                                                              • not ((List.hd b.b_buys).o_qty < (List.hd b.b_sells).o_qty)
                                                                                                                                              • (List.hd b.b_buys).o_price >= (List.hd b.b_sells).o_price
                                                                                                                                              • not Is_a([], b.b_buys)
                                                                                                                                              • not Is_a([], b.b_sells)
                                                                                                                                              let (_x_0 : order list) = b.b_buys in
                                                                                                                                              let (_x_1 : order) = List.hd _x_0 in
                                                                                                                                              let (_x_2 : order list) = b.b_sells in
                                                                                                                                              let (_x_3 : order) = List.hd _x_2 in
                                                                                                                                              let (_x_4 : int) = _x_3.o_qty in
                                                                                                                                              let (_x_5 : int) = (_x_1.o_price + _x_3.o_price) / 2 in
                                                                                                                                              uncross_book
                                                                                                                                              {b_buys = {_x_1 with o_qty = _x_1.o_qty - _x_4} :: (List.tl _x_0);
                                                                                                                                               b_sells = List.tl _x_2}
                                                                                                                                              ({fill_client_id = _x_3.o_client_id; fill_qty = _x_4; fill_price = _x_5;
                                                                                                                                                fill_order_id = _x_3.o_id; fill_order_done = true}
                                                                                                                                               ::
                                                                                                                                               ({fill_client_id = _x_1.o_client_id; fill_qty = _x_4; fill_price = _x_5;
                                                                                                                                                 fill_order_id = _x_1.o_id; fill_order_done = true}
                                                                                                                                                :: fills))
                                                                                                                                              (filled_qty + _x_4)
                                                                                                                                              3
                                                                                                                                              • fills = []
                                                                                                                                              • filled_qty = 0
                                                                                                                                              • (List.hd b.b_buys).o_is_implied
                                                                                                                                              • not (List.hd b.b_sells).o_is_implied
                                                                                                                                              • not ((List.hd b.b_buys).o_qty - (List.hd b.b_sells).o_qty = 0)
                                                                                                                                              • not ((List.hd b.b_buys).o_qty < (List.hd b.b_sells).o_qty)
                                                                                                                                              • (List.hd b.b_buys).o_price >= (List.hd b.b_sells).o_price
                                                                                                                                              • not Is_a([], b.b_buys)
                                                                                                                                              • not Is_a([], b.b_sells)
                                                                                                                                              let (_x_0 : order list) = b.b_buys in
                                                                                                                                              let (_x_1 : order) = List.hd _x_0 in
                                                                                                                                              let (_x_2 : order list) = b.b_sells in
                                                                                                                                              let (_x_3 : order) = List.hd _x_2 in
                                                                                                                                              let (_x_4 : int) = _x_3.o_qty in
                                                                                                                                              uncross_book
                                                                                                                                              {b_buys = {_x_1 with o_qty = _x_1.o_qty - _x_4} :: (List.tl _x_0);
                                                                                                                                               b_sells = List.tl _x_2}
                                                                                                                                              ({fill_client_id = _x_3.o_client_id; fill_qty = _x_4;
                                                                                                                                                fill_price = (_x_1.o_price + _x_3.o_price) / 2; fill_order_id = _x_3.o_id;
                                                                                                                                                fill_order_done = true}
                                                                                                                                               :: fills)
                                                                                                                                              (filled_qty + _x_4)
                                                                                                                                              2
                                                                                                                                              • fills = []
                                                                                                                                              • filled_qty = 0
                                                                                                                                              • not (List.hd b.b_buys).o_is_implied
                                                                                                                                              • (List.hd b.b_sells).o_is_implied
                                                                                                                                              • not ((List.hd b.b_buys).o_qty - (List.hd b.b_sells).o_qty = 0)
                                                                                                                                              • not ((List.hd b.b_buys).o_qty < (List.hd b.b_sells).o_qty)
                                                                                                                                              • (List.hd b.b_buys).o_price >= (List.hd b.b_sells).o_price
                                                                                                                                              • not Is_a([], b.b_buys)
                                                                                                                                              • not Is_a([], b.b_sells)
                                                                                                                                              let (_x_0 : order list) = b.b_buys in
                                                                                                                                              let (_x_1 : order) = List.hd _x_0 in
                                                                                                                                              let (_x_2 : order list) = b.b_sells in
                                                                                                                                              let (_x_3 : order) = List.hd _x_2 in
                                                                                                                                              let (_x_4 : int) = _x_3.o_qty in
                                                                                                                                              uncross_book
                                                                                                                                              {b_buys = {_x_1 with o_qty = _x_1.o_qty - _x_4} :: (List.tl _x_0);
                                                                                                                                               b_sells = List.tl _x_2}
                                                                                                                                              ({fill_client_id = _x_1.o_client_id; fill_qty = _x_4;
                                                                                                                                                fill_price = (_x_1.o_price + _x_3.o_price) / 2; fill_order_id = _x_1.o_id;
                                                                                                                                                fill_order_done = true}
                                                                                                                                               :: fills)
                                                                                                                                              (filled_qty + _x_4)
                                                                                                                                              1
                                                                                                                                              • fills = []
                                                                                                                                              • filled_qty = 0
                                                                                                                                              • (List.hd b.b_buys).o_is_implied
                                                                                                                                              • (List.hd b.b_sells).o_is_implied
                                                                                                                                              • not ((List.hd b.b_buys).o_qty - (List.hd b.b_sells).o_qty = 0)
                                                                                                                                              • not ((List.hd b.b_buys).o_qty < (List.hd b.b_sells).o_qty)
                                                                                                                                              • (List.hd b.b_buys).o_price >= (List.hd b.b_sells).o_price
                                                                                                                                              • not Is_a([], b.b_buys)
                                                                                                                                              • not Is_a([], b.b_sells)
                                                                                                                                              let (_x_0 : order list) = b.b_buys in
                                                                                                                                              let (_x_1 : order) = List.hd _x_0 in
                                                                                                                                              let (_x_2 : order list) = b.b_sells in
                                                                                                                                              let (_x_3 : int) = (List.hd _x_2).o_qty in
                                                                                                                                              uncross_book
                                                                                                                                              {b_buys = {_x_1 with o_qty = _x_1.o_qty - _x_3} :: (List.tl _x_0);
                                                                                                                                               b_sells = List.tl _x_2}
                                                                                                                                              fills (filled_qty + _x_3)
                                                                                                                                              0
                                                                                                                                              • fills = []
                                                                                                                                              • filled_qty = 0
                                                                                                                                              • not ((List.hd b.b_buys).o_price >= (List.hd b.b_sells).o_price)
                                                                                                                                              • not Is_a([], b.b_buys)
                                                                                                                                              • not Is_a([], b.b_sells)
                                                                                                                                              {uncrossed_book = b; uncrossed_fills = fills; uncrossed_qty = filled_qty}
                                                                                                                                              In [10]:
                                                                                                                                              (* Now let's try to generate some test cases *)
                                                                                                                                              
                                                                                                                                              (* This will auto-generate model extractor *)
                                                                                                                                              Extract.eval ~quiet:true ~signature:(Event.DB.fun_id_of_str "uncross_book") ();;
                                                                                                                                              
                                                                                                                                              #remove_doc doc_of_book;;
                                                                                                                                              #remove_doc doc_of_order;;
                                                                                                                                              Modular_decomp.get_regions d |> CCList.map (fun r -> r |> Modular_decomp.get_model |> Mex.of_model);;
                                                                                                                                              #install_doc doc_of_order;;
                                                                                                                                              #install_doc doc_of_book;;
                                                                                                                                              
                                                                                                                                              Out[10]:
                                                                                                                                                                                  - : unit = ()
                                                                                                                                              Unbound value doc_pp_doc_of_book.
                                                                                                                                              Unbound value doc_pp_doc_of_book.
                                                                                                                                              Unbound value doc_pp_doc_of_order.
                                                                                                                                              Unbound value doc_pp_doc_of_order.
                                                                                                                                              - : Mex.extract_type list =
                                                                                                                                              [{Mex.b = {b_buys = []; b_sells = []}; fills = []; filled_qty = 0};
                                                                                                                                               {Mex.b =
                                                                                                                                                 {b_buys =
                                                                                                                                                   [{o_qty = 2; o_price = 3; o_time = 4; o_id = 5; o_side = BUY;
                                                                                                                                                     o_client_id = 6; o_inst = Strategy STRAT1; o_is_implied = false}];
                                                                                                                                                  b_sells = []};
                                                                                                                                                fills = []; filled_qty = 0};
                                                                                                                                               {Mex.b =
                                                                                                                                                 {b_buys = [];
                                                                                                                                                  b_sells =
                                                                                                                                                   [{o_qty = 3; o_price = 4; o_time = 2; o_id = 5; o_side = BUY;
                                                                                                                                                     o_client_id = 6; o_inst = Strategy STRAT1; o_is_implied = false}]};
                                                                                                                                                fills = []; filled_qty = 0};
                                                                                                                                               {Mex.b =
                                                                                                                                                 {b_buys =
                                                                                                                                                   [{o_qty = 0; o_price = 21238; o_time = 2; o_id = 3; o_side = BUY;
                                                                                                                                                     o_client_id = 4; o_inst = Strategy STRAT1; o_is_implied = false}];
                                                                                                                                                  b_sells =
                                                                                                                                                   [{o_qty = 1; o_price = -7719; o_time = 6; o_id = 7; o_side = BUY;
                                                                                                                                                     o_client_id = 5; o_inst = Strategy STRAT1; o_is_implied = false}]};
                                                                                                                                                fills = []; filled_qty = 0};
                                                                                                                                               {Mex.b =
                                                                                                                                                 {b_buys =
                                                                                                                                                   [{o_qty = 0; o_price = 21238; o_time = 2; o_id = 3; o_side = BUY;
                                                                                                                                                     o_client_id = 4; o_inst = Strategy STRAT1; o_is_implied = true}];
                                                                                                                                                  b_sells =
                                                                                                                                                   [{o_qty = 1; o_price = -7719; o_time = 6; o_id = 7; o_side = BUY;
                                                                                                                                                     o_client_id = 5; o_inst = Strategy STRAT1; o_is_implied = false}]};
                                                                                                                                                fills = []; filled_qty = 0};
                                                                                                                                               {Mex.b =
                                                                                                                                                 {b_buys =
                                                                                                                                                   [{o_qty = 0; o_price = 21238; o_time = 2; o_id = 3; o_side = BUY;
                                                                                                                                                     o_client_id = 4; o_inst = Strategy STRAT1; o_is_implied = false}];
                                                                                                                                                  b_sells =
                                                                                                                                                   [{o_qty = 1; o_price = -7719; o_time = 5; o_id = 6; o_side = BUY;
                                                                                                                                                     o_client_id = 7; o_inst = Strategy STRAT1; o_is_implied = true}]};
                                                                                                                                                fills = []; filled_qty = 0};
                                                                                                                                               {Mex.b =
                                                                                                                                                 {b_buys =
                                                                                                                                                   [{o_qty = 0; o_price = 21238; o_time = 2; o_id = 3; o_side = BUY;
                                                                                                                                                     o_client_id = 4; o_inst = Strategy STRAT1; o_is_implied = true}];
                                                                                                                                                  b_sells =
                                                                                                                                                   [{o_qty = 1; o_price = -7719; o_time = 6; o_id = 7; o_side = BUY;
                                                                                                                                                     o_client_id = 5; o_inst = Strategy STRAT1; o_is_implied = true}]};
                                                                                                                                                fills = []; filled_qty = 0};
                                                                                                                                               {Mex.b =
                                                                                                                                                 {b_buys =
                                                                                                                                                   [{o_qty = 0; o_price = 7719; o_time = 3; o_id = 2; o_side = BUY;
                                                                                                                                                     o_client_id = 4; o_inst = Strategy STRAT1; o_is_implied = false}];
                                                                                                                                                  b_sells =
                                                                                                                                                   [{o_qty = 0; o_price = -38; o_time = 5; o_id = 6; o_side = BUY;
                                                                                                                                                     o_client_id = 7; o_inst = Strategy STRAT1; o_is_implied = false}]};
                                                                                                                                                fills = []; filled_qty = 0};
                                                                                                                                               {Mex.b =
                                                                                                                                                 {b_buys =
                                                                                                                                                   [{o_qty = 0; o_price = 7719; o_time = 2; o_id = 3; o_side = BUY;
                                                                                                                                                     o_client_id = 4; o_inst = Strategy STRAT1; o_is_implied = true}];
                                                                                                                                                  b_sells =
                                                                                                                                                   [{o_qty = 0; o_price = -38; o_time = 5; o_id = 6; o_side = BUY;
                                                                                                                                                     o_client_id = 7; o_inst = Strategy STRAT1; o_is_implied = false}]};
                                                                                                                                                fills = []; filled_qty = 0};
                                                                                                                                               {Mex.b =
                                                                                                                                                 {b_buys =
                                                                                                                                                   [{o_qty = 0; o_price = 7719; o_time = 2; o_id = 3; o_side = BUY;
                                                                                                                                                     o_client_id = 4; o_inst = Strategy STRAT1; o_is_implied = false}];
                                                                                                                                                  b_sells =
                                                                                                                                                   [{o_qty = 0; o_price = -38; o_time = 6; o_id = 5; o_side = BUY;
                                                                                                                                                     o_client_id = 7; o_inst = Strategy STRAT1; o_is_implied = true}]};
                                                                                                                                                fills = []; filled_qty = 0};
                                                                                                                                               {Mex.b =
                                                                                                                                                 {b_buys =
                                                                                                                                                   [{o_qty = 0; o_price = 7719; o_time = 2; o_id = 3; o_side = BUY;
                                                                                                                                                     o_client_id = 4; o_inst = Strategy STRAT1; o_is_implied = true}];
                                                                                                                                                  b_sells =
                                                                                                                                                   [{o_qty = 0; o_price = -38; o_time = 5; o_id = 6; o_side = BUY;
                                                                                                                                                     o_client_id = 7; o_inst = Strategy STRAT1; o_is_implied = true}]};
                                                                                                                                                fills = []; filled_qty = 0};
                                                                                                                                               {Mex.b =
                                                                                                                                                 {b_buys =
                                                                                                                                                   [{o_qty = 0; o_price = 21238; o_time = 2; o_id = 3; o_side = BUY;
                                                                                                                                                     o_client_id = 4; o_inst = Strategy STRAT1; o_is_implied = false}];
                                                                                                                                                  b_sells =
                                                                                                                                                   [{o_qty = -1; o_price = -7719; o_time = 5; o_id = 6; o_side = BUY;
                                                                                                                                                     o_client_id = 7; o_inst = Strategy STRAT1; o_is_implied = false}]};
                                                                                                                                                fills = []; filled_qty = 0};
                                                                                                                                               {Mex.b =
                                                                                                                                                 {b_buys =
                                                                                                                                                   [{o_qty = 0; o_price = 21238; o_time = 2; o_id = 3; o_side = BUY;
                                                                                                                                                     o_client_id = 4; o_inst = Strategy STRAT1; o_is_implied = true}];
                                                                                                                                                  b_sells =
                                                                                                                                                   [{o_qty = -1; o_price = -7719; o_time = 5; o_id = 6; o_side = BUY;
                                                                                                                                                     o_client_id = 7; o_inst = Strategy STRAT1; o_is_implied = false}]};
                                                                                                                                                fills = []; filled_qty = 0};{Mex.b = ...; fills = ...; filled_qty = ...};
                                                                                                                                               ...;...]
                                                                                                                                              Line 2, characters 18-30:
                                                                                                                                              2 |           let d = doc_of_order x in
                                                                                                                                                                    ^^^^^^^^^^^^
                                                                                                                                              Error: Unbound value doc_of_order
                                                                                                                                              Line 2, characters 18-29:
                                                                                                                                              2 |           let d = doc_of_book x in
                                                                                                                                                                    ^^^^^^^^^^^
                                                                                                                                              Error: Unbound value doc_of_book
                                                                                                                                              

                                                                                                                                              3 Implied trading

                                                                                                                                              3.1 Strategy ranking

                                                                                                                                              When generating implied orders for strategies, there's a criteria used to rank strategies - this section encodes the comparison function.

                                                                                                                                              In [11]:
                                                                                                                                              (* Calculate somehow how big the ratio is *)
                                                                                                                                              let leg_ratio (s : strategy) =
                                                                                                                                                let abs x = if x < 0 then -x else x in
                                                                                                                                                (abs s.leg1.leg_mult) + (abs s.leg2.leg_mult) + (abs s.leg3.leg_mult)
                                                                                                                                              ;;
                                                                                                                                              
                                                                                                                                              (* Nearest time to expiry *)
                                                                                                                                              let nearest_time_to_exp (s : strategy) =
                                                                                                                                                let exp =
                                                                                                                                                  if (month_to_int (contract_expiry s.leg1.leg_sec_idx)) < (month_to_int (contract_expiry s.leg2.leg_sec_idx)) then
                                                                                                                                                    contract_expiry s.leg1.leg_sec_idx
                                                                                                                                                  else
                                                                                                                                                    contract_expiry s.leg2.leg_sec_idx in
                                                                                                                                              
                                                                                                                                                if (month_to_int exp) < (month_to_int (contract_expiry s.leg2.leg_sec_idx)) then
                                                                                                                                                  exp
                                                                                                                                                else
                                                                                                                                                  contract_expiry s.leg2.leg_sec_idx
                                                                                                                                              ;;
                                                                                                                                              
                                                                                                                                              (* Return true if s1 should implied uncross before s2 *)
                                                                                                                                              let priority_strat (s1 : strategy) (s2 : strategy) =
                                                                                                                                                (*
                                                                                                                                                  1. time to expiry of the nearest leg
                                                                                                                                                  2. strategy types (strategies with the greater leg ratio executed first)
                                                                                                                                                  3. strategy creation times *)
                                                                                                                                                if (month_to_int (nearest_time_to_exp s1)) < (month_to_int (nearest_time_to_exp s2)) then
                                                                                                                                                  true
                                                                                                                                                else
                                                                                                                                                  if (leg_ratio s1) > (leg_ratio s2) then
                                                                                                                                                    true
                                                                                                                                                  else
                                                                                                                                                    s1.time_created <= s2.time_created
                                                                                                                                              
                                                                                                                                              Out[11]:
                                                                                                                                              val leg_ratio : strategy -> int = <fun>
                                                                                                                                              val nearest_time_to_exp : strategy -> month = <fun>
                                                                                                                                              val priority_strat : strategy -> strategy -> bool = <fun>
                                                                                                                                              
                                                                                                                                              In [12]:
                                                                                                                                              let transitivity s1 s2 s3 =
                                                                                                                                               ((priority_strat s1 s2) && (priority_strat s2 s3)) ==> (priority_strat s1 s3)
                                                                                                                                              
                                                                                                                                              verify transitivity
                                                                                                                                              
                                                                                                                                              Out[12]:
                                                                                                                                              val transitivity : strategy -> strategy -> strategy -> bool = <fun>
                                                                                                                                              - : strategy -> strategy -> strategy -> bool = <fun>
                                                                                                                                              module CX : sig val s1 : strategy val s2 : strategy val s3 : strategy end
                                                                                                                                              
                                                                                                                                              Counterexample (after 0 steps, 0.036s):
                                                                                                                                               let (s1 : strategy) =
                                                                                                                                                {time_created = 0; leg1 = {leg_sec_idx = OUT1; leg_mult = 0};
                                                                                                                                                 leg2 = {leg_sec_idx = OUT3; leg_mult = 1};
                                                                                                                                                 leg3 = {leg_sec_idx = OUT1; leg_mult = 0}}
                                                                                                                                               let (s2 : strategy) =
                                                                                                                                                {time_created = (-2998); leg1 = {leg_sec_idx = OUT3; leg_mult = 0};
                                                                                                                                                 leg2 = {leg_sec_idx = OUT1; leg_mult = 0};
                                                                                                                                                 leg3 = {leg_sec_idx = OUT1; leg_mult = 0}}
                                                                                                                                               let (s3 : strategy) =
                                                                                                                                                {time_created = (-1); leg1 = {leg_sec_idx = OUT1; leg_mult = 0};
                                                                                                                                                 leg2 = {leg_sec_idx = OUT2; leg_mult = 0};
                                                                                                                                                 leg3 = {leg_sec_idx = OUT1; leg_mult = (-1)}}
                                                                                                                                              
                                                                                                                                              Refuted
                                                                                                                                              proof attempt
                                                                                                                                              ground_instances0
                                                                                                                                              definitions0
                                                                                                                                              inductions0
                                                                                                                                              search_time
                                                                                                                                              0.036s
                                                                                                                                              details
                                                                                                                                              Expand
                                                                                                                                              smt_stats
                                                                                                                                              num checks1
                                                                                                                                              arith-assume-eqs9
                                                                                                                                              arith-make-feasible327
                                                                                                                                              arith-max-columns77
                                                                                                                                              arith-conflicts6
                                                                                                                                              rlimit count21444
                                                                                                                                              arith-cheap-eqs38
                                                                                                                                              mk clause745
                                                                                                                                              datatype occurs check63
                                                                                                                                              mk bool var985
                                                                                                                                              arith-lower200
                                                                                                                                              arith-diseq67
                                                                                                                                              datatype splits165
                                                                                                                                              decisions627
                                                                                                                                              arith-propagations122
                                                                                                                                              propagations905
                                                                                                                                              interface eqs9
                                                                                                                                              arith-bound-propagations-cheap122
                                                                                                                                              arith-max-rows39
                                                                                                                                              conflicts55
                                                                                                                                              datatype accessor ax59
                                                                                                                                              minimized lits10
                                                                                                                                              arith-bound-propagations-lp23
                                                                                                                                              datatype constructor ax217
                                                                                                                                              num allocs1372558893
                                                                                                                                              final checks10
                                                                                                                                              added eqs1671
                                                                                                                                              del clause303
                                                                                                                                              arith eq adapter226
                                                                                                                                              arith-upper328
                                                                                                                                              time0.024000
                                                                                                                                              memory33.810000
                                                                                                                                              max memory78.250000
                                                                                                                                              Expand
                                                                                                                                              • start[0.036s]
                                                                                                                                                  let (_x_0 : int) = ( :var_0: ).time_created in
                                                                                                                                                  let (_x_1 : int) = ( :var_1: ).time_created in
                                                                                                                                                  let (_x_2 : int) = ( :var_0: ).leg1.leg_mult in
                                                                                                                                                  let (_x_3 : int) = ( :var_0: ).leg2.leg_mult in
                                                                                                                                                  let (_x_4 : int) = ( :var_0: ).leg3.leg_mult in
                                                                                                                                                  let (_x_5 : int)
                                                                                                                                                      = (if _x_2 < 0 then ~- _x_2 else _x_2)
                                                                                                                                                        + (if _x_3 < 0 then ~- _x_3 else _x_3)
                                                                                                                                                        + (if _x_4 < 0 then ~- _x_4 else _x_4)
                                                                                                                                                  in
                                                                                                                                                  let (_x_6 : int) = ( :var_1: ).leg1.leg_mult in
                                                                                                                                                  let (_x_7 : int) = ( :var_1: ).leg2.leg_mult in
                                                                                                                                                  let (_x_8 : int) = ( :var_1: ).leg3.leg_mult in
                                                                                                                                                  let (_x_9 : int)
                                                                                                                                                      = (if _x_6 < 0 then ~- _x_6 else _x_6)
                                                                                                                                                        + (if _x_7 < 0 then ~- _x_7 else _x_7)
                                                                                                                                                        + (if _x_8 < 0 then ~- _x_8 else _x_8)
                                                                                                                                                  in
                                                                                                                                                  let (_x_10 : bool) = Is_a(OUT1, …) in
                                                                                                                                                  let (_x_11 : bool) = Is_a(Jun, …) in
                                                                                                                                                  let (_x_12 : bool) = Is_a(OUT1, …) in
                                                                                                                                                  let (_x_13 : bool) = Is_a(Mar, if _x_12 then … else …) in
                                                                                                                                                  let (_x_14 : bool)
                                                                                                                                                      = (if Is_a(Mar, if _x_10 then … else …) then 3
                                                                                                                                                         else if Is_a(Jun, …) then 6 else …)
                                                                                                                                                        < (if _x_13 then 3 else if _x_11 then 6 else …)
                                                                                                                                                  in
                                                                                                                                                  let (_x_15 : bool)
                                                                                                                                                      = (if Is_a(Mar,
                                                                                                                                                            if _x_14 then if _x_10 then … else …
                                                                                                                                                            else if _x_12 then … else …)
                                                                                                                                                         then 3
                                                                                                                                                         else
                                                                                                                                                         if Is_a(Jun, if _x_14 then … else …) then 6
                                                                                                                                                         else if Is_a(Sep, …) then 9 else 12)
                                                                                                                                                        <
                                                                                                                                                        (if _x_13 then 3
                                                                                                                                                         else if _x_11 then 6 else if Is_a(Sep, …) then 9 else 12)
                                                                                                                                                  in
                                                                                                                                                  let (_x_16 : int)
                                                                                                                                                      = if Is_a(Mar,
                                                                                                                                                           if _x_15
                                                                                                                                                           then
                                                                                                                                                             if _x_14 then if _x_10 then … else …
                                                                                                                                                             else if _x_12 then … else …
                                                                                                                                                           else if _x_12 then … else if Is_a(OUT2, …) then … else …)
                                                                                                                                                        then 3
                                                                                                                                                        else
                                                                                                                                                        if Is_a(Jun,
                                                                                                                                                           if _x_15 then if _x_14 then … else …
                                                                                                                                                           else if _x_12 then … else …)
                                                                                                                                                        then 6 else if Is_a(Sep, if _x_15 then … else …) then 9 else 12
                                                                                                                                                  in
                                                                                                                                                  let (_x_17 : bool) = Is_a(OUT1, …) in
                                                                                                                                                  let (_x_18 : bool) = Is_a(Jun, …) in
                                                                                                                                                  let (_x_19 : bool) = Is_a(OUT1, …) in
                                                                                                                                                  let (_x_20 : bool) = Is_a(Mar, if _x_19 then … else …) in
                                                                                                                                                  let (_x_21 : bool)
                                                                                                                                                      = (if Is_a(Mar, if _x_17 then … else …) then 3
                                                                                                                                                         else if Is_a(Jun, …) then 6 else …)
                                                                                                                                                        < (if _x_20 then 3 else if _x_18 then 6 else …)
                                                                                                                                                  in
                                                                                                                                                  let (_x_22 : bool)
                                                                                                                                                      = (if Is_a(Mar,
                                                                                                                                                            if _x_21 then if _x_17 then … else …
                                                                                                                                                            else if _x_19 then … else …)
                                                                                                                                                         then 3
                                                                                                                                                         else
                                                                                                                                                         if Is_a(Jun, if _x_21 then … else …) then 6
                                                                                                                                                         else if Is_a(Sep, …) then 9 else 12)
                                                                                                                                                        <
                                                                                                                                                        (if _x_20 then 3
                                                                                                                                                         else if _x_18 then 6 else if Is_a(Sep, …) then 9 else 12)
                                                                                                                                                  in
                                                                                                                                                  let (_x_23 : int)
                                                                                                                                                      = if Is_a(Mar,
                                                                                                                                                           if _x_22
                                                                                                                                                           then
                                                                                                                                                             if _x_21 then if _x_17 then … else …
                                                                                                                                                             else if _x_19 then … else …
                                                                                                                                                           else if _x_19 then … else if Is_a(OUT2, …) then … else …)
                                                                                                                                                        then 3
                                                                                                                                                        else
                                                                                                                                                        if Is_a(Jun,
                                                                                                                                                           if _x_22 then if _x_21 then … else …
                                                                                                                                                           else if _x_19 then … else …)
                                                                                                                                                        then 6 else if Is_a(Sep, if _x_22 then … else …) then 9 else 12
                                                                                                                                                  in
                                                                                                                                                  let (_x_24 : int) = ( :var_2: ).time_created in
                                                                                                                                                  let (_x_25 : int) = ( :var_2: ).leg1.leg_mult in
                                                                                                                                                  let (_x_26 : int) = ( :var_2: ).leg2.leg_mult in
                                                                                                                                                  let (_x_27 : int) = ( :var_2: ).leg3.leg_mult in
                                                                                                                                                  let (_x_28 : int)
                                                                                                                                                      = (if _x_25 < 0 then ~- _x_25 else _x_25)
                                                                                                                                                        + (if _x_26 < 0 then ~- _x_26 else _x_26)
                                                                                                                                                        + (if _x_27 < 0 then ~- _x_27 else _x_27)
                                                                                                                                                  in
                                                                                                                                                  let (_x_29 : bool) = Is_a(OUT1, …) in
                                                                                                                                                  let (_x_30 : bool) = Is_a(Jun, …) in
                                                                                                                                                  let (_x_31 : bool) = Is_a(OUT1, …) in
                                                                                                                                                  let (_x_32 : bool) = Is_a(Mar, if _x_31 then … else …) in
                                                                                                                                                  let (_x_33 : bool)
                                                                                                                                                      = (if Is_a(Mar, if _x_29 then … else …) then 3
                                                                                                                                                         else if Is_a(Jun, …) then 6 else …)
                                                                                                                                                        < (if _x_32 then 3 else if _x_30 then 6 else …)
                                                                                                                                                  in
                                                                                                                                                  let (_x_34 : bool)
                                                                                                                                                      = (if Is_a(Mar,
                                                                                                                                                            if _x_33 then if _x_29 then … else …
                                                                                                                                                            else if _x_31 then … else …)
                                                                                                                                                         then 3
                                                                                                                                                         else
                                                                                                                                                         if Is_a(Jun, if _x_33 then … else …) then 6
                                                                                                                                                         else if Is_a(Sep, …) then 9 else 12)
                                                                                                                                                        <
                                                                                                                                                        (if _x_32 then 3
                                                                                                                                                         else if _x_30 then 6 else if Is_a(Sep, …) then 9 else 12)
                                                                                                                                                  in
                                                                                                                                                  let (_x_35 : int)
                                                                                                                                                      = if Is_a(Mar,
                                                                                                                                                           if _x_34
                                                                                                                                                           then
                                                                                                                                                             if _x_33 then if _x_29 then … else …
                                                                                                                                                             else if _x_31 then … else …
                                                                                                                                                           else if _x_31 then … else if Is_a(OUT2, …) then … else …)
                                                                                                                                                        then 3
                                                                                                                                                        else
                                                                                                                                                        if Is_a(Jun,
                                                                                                                                                           if _x_34 then if _x_33 then … else …
                                                                                                                                                           else if _x_31 then … else …)
                                                                                                                                                        then 6 else if Is_a(Sep, if _x_34 then … else …) then 9 else 12
                                                                                                                                                  in
                                                                                                                                                  (if _x_16 < _x_23 then true else if _x_5 > _x_9 then true else _x_0 <= _x_1)
                                                                                                                                                  && (if _x_23 < _x_35 then true
                                                                                                                                                      else if _x_9 > _x_28 then true else _x_1 <= _x_24)
                                                                                                                                                  ==> (if _x_16 < _x_35 then true
                                                                                                                                                       else if _x_5 > _x_28 then true else _x_0 <= _x_24)
                                                                                                                                              • simplify

                                                                                                                                                into
                                                                                                                                                let (_x_0 : int) = ( :var_0: ).time_created in
                                                                                                                                                let (_x_1 : int) = ( :var_2: ).time_created in
                                                                                                                                                let (_x_2 : outright_id) = ….leg_sec_idx in
                                                                                                                                                let (_x_3 : bool) = Is_a(OUT1, _x_2) in
                                                                                                                                                let (_x_4 : month)
                                                                                                                                                    = if _x_3 then Mar else if Is_a(OUT2, _x_2) then … else …
                                                                                                                                                in
                                                                                                                                                let (_x_5 : int)
                                                                                                                                                    = if Is_a(Mar, _x_4) then 3
                                                                                                                                                      else
                                                                                                                                                      if Is_a(Jun, if _x_3 then Mar else …) then 6
                                                                                                                                                      else if Is_a(Sep, …) then 9 else 12
                                                                                                                                                in
                                                                                                                                                let (_x_6 : outright_id) = ….leg_sec_idx in
                                                                                                                                                let (_x_7 : bool) = Is_a(OUT1, _x_6) in
                                                                                                                                                let (_x_8 : month)
                                                                                                                                                    = if _x_7 then Mar else if Is_a(OUT2, _x_6) then … else …
                                                                                                                                                in
                                                                                                                                                let (_x_9 : bool)
                                                                                                                                                    = _x_5 <=
                                                                                                                                                      (if Is_a(Mar, _x_8) then 3
                                                                                                                                                       else
                                                                                                                                                       if Is_a(Jun, if _x_7 then Mar else …) then 6
                                                                                                                                                       else if Is_a(Sep, …) then 9 else 12)
                                                                                                                                                in
                                                                                                                                                let (_x_10 : bool)
                                                                                                                                                    = _x_9
                                                                                                                                                      || _x_5 <=
                                                                                                                                                         (if Is_a(Mar,
                                                                                                                                                             if _x_9 then if _x_3 then Mar else …
                                                                                                                                                             else if _x_7 then Mar else …)
                                                                                                                                                          then 3
                                                                                                                                                          else
                                                                                                                                                          if Is_a(Jun, if _x_9 then … else …) then 6
                                                                                                                                                          else if Is_a(Sep, …) then 9 else 12)
                                                                                                                                                in
                                                                                                                                                let (_x_11 : int)
                                                                                                                                                    = if Is_a(Mar, if _x_10 then _x_4 else _x_8) then 3
                                                                                                                                                      else
                                                                                                                                                      if Is_a(Jun,
                                                                                                                                                         if _x_10 then if _x_3 then Mar else …
                                                                                                                                                         else if _x_7 then Mar else …)
                                                                                                                                                      then 6 else if Is_a(Sep, if _x_10 then … else …) then 9 else 12
                                                                                                                                                in
                                                                                                                                                let (_x_12 : outright_id) = ….leg_sec_idx in
                                                                                                                                                let (_x_13 : bool) = Is_a(OUT1, _x_12) in
                                                                                                                                                let (_x_14 : month)
                                                                                                                                                    = if _x_13 then Mar else if Is_a(OUT2, _x_12) then … else …
                                                                                                                                                in
                                                                                                                                                let (_x_15 : int)
                                                                                                                                                    = if Is_a(Mar, _x_14) then 3
                                                                                                                                                      else
                                                                                                                                                      if Is_a(Jun, if _x_13 then Mar else …) then 6
                                                                                                                                                      else if Is_a(Sep, …) then 9 else 12
                                                                                                                                                in
                                                                                                                                                let (_x_16 : outright_id) = ….leg_sec_idx in
                                                                                                                                                let (_x_17 : bool) = Is_a(OUT1, _x_16) in
                                                                                                                                                let (_x_18 : month)
                                                                                                                                                    = if _x_17 then Mar else if Is_a(OUT2, _x_16) then … else …
                                                                                                                                                in
                                                                                                                                                let (_x_19 : bool)
                                                                                                                                                    = _x_15 <=
                                                                                                                                                      (if Is_a(Mar, _x_18) then 3
                                                                                                                                                       else
                                                                                                                                                       if Is_a(Jun, if _x_17 then Mar else …) then 6
                                                                                                                                                       else if Is_a(Sep, …) then 9 else 12)
                                                                                                                                                in
                                                                                                                                                let (_x_20 : bool)
                                                                                                                                                    = _x_19
                                                                                                                                                      || _x_15 <=
                                                                                                                                                         (if Is_a(Mar,
                                                                                                                                                             if _x_19 then if _x_13 then Mar else …
                                                                                                                                                             else if _x_17 then Mar else …)
                                                                                                                                                          then 3
                                                                                                                                                          else
                                                                                                                                                          if Is_a(Jun, if _x_19 then … else …) then 6
                                                                                                                                                          else if Is_a(Sep, …) then 9 else 12)
                                                                                                                                                in
                                                                                                                                                let (_x_21 : int)
                                                                                                                                                    = if Is_a(Mar, if _x_20 then _x_14 else _x_18) then 3
                                                                                                                                                      else
                                                                                                                                                      if Is_a(Jun,
                                                                                                                                                         if _x_20 then if _x_13 then Mar else …
                                                                                                                                                         else if _x_17 then Mar else …)
                                                                                                                                                      then 6 else if Is_a(Sep, if _x_20 then … else …) then 9 else 12
                                                                                                                                                in
                                                                                                                                                let (_x_22 : int) = ….leg_mult in
                                                                                                                                                let (_x_23 : int) = ….leg_mult in
                                                                                                                                                let (_x_24 : int) = ( :var_0: ).leg3.leg_mult in
                                                                                                                                                let (_x_25 : int)
                                                                                                                                                    = (if 0 <= _x_22 then _x_22 else -1 * _x_22)
                                                                                                                                                      + (if 0 <= _x_23 then _x_23 else -1 * _x_23)
                                                                                                                                                      + (if 0 <= _x_24 then _x_24 else -1 * _x_24)
                                                                                                                                                in
                                                                                                                                                let (_x_26 : int) = ….leg_mult in
                                                                                                                                                let (_x_27 : int) = ….leg_mult in
                                                                                                                                                let (_x_28 : int) = ( :var_2: ).leg3.leg_mult in
                                                                                                                                                let (_x_29 : int)
                                                                                                                                                    = (if 0 <= _x_26 then _x_26 else -1 * _x_26)
                                                                                                                                                      + (if 0 <= _x_27 then _x_27 else -1 * _x_27)
                                                                                                                                                      + (if 0 <= _x_28 then _x_28 else -1 * _x_28)
                                                                                                                                                in
                                                                                                                                                let (_x_30 : int) = ( :var_1: ).time_created in
                                                                                                                                                let (_x_31 : outright_id) = ….leg_sec_idx in
                                                                                                                                                let (_x_32 : bool) = Is_a(OUT1, _x_31) in
                                                                                                                                                let (_x_33 : month)
                                                                                                                                                    = if _x_32 then Mar else if Is_a(OUT2, _x_31) then … else …
                                                                                                                                                in
                                                                                                                                                let (_x_34 : int)
                                                                                                                                                    = if Is_a(Mar, _x_33) then 3
                                                                                                                                                      else
                                                                                                                                                      if Is_a(Jun, if _x_32 then Mar else …) then 6
                                                                                                                                                      else if Is_a(Sep, …) then 9 else 12
                                                                                                                                                in
                                                                                                                                                let (_x_35 : outright_id) = ….leg_sec_idx in
                                                                                                                                                let (_x_36 : bool) = Is_a(OUT1, _x_35) in
                                                                                                                                                let (_x_37 : month)
                                                                                                                                                    = if _x_36 then Mar else if Is_a(OUT2, _x_35) then … else …
                                                                                                                                                in
                                                                                                                                                let (_x_38 : bool)
                                                                                                                                                    = _x_34 <=
                                                                                                                                                      (if Is_a(Mar, _x_37) then 3
                                                                                                                                                       else
                                                                                                                                                       if Is_a(Jun, if _x_36 then Mar else …) then 6
                                                                                                                                                       else if Is_a(Sep, …) then 9 else 12)
                                                                                                                                                in
                                                                                                                                                let (_x_39 : bool)
                                                                                                                                                    = _x_38
                                                                                                                                                      || _x_34 <=
                                                                                                                                                         (if Is_a(Mar,
                                                                                                                                                             if _x_38 then if _x_32 then Mar else …
                                                                                                                                                             else if _x_36 then Mar else …)
                                                                                                                                                          then 3
                                                                                                                                                          else
                                                                                                                                                          if Is_a(Jun, if _x_38 then … else …) then 6
                                                                                                                                                          else if Is_a(Sep, …) then 9 else 12)
                                                                                                                                                in
                                                                                                                                                let (_x_40 : int)
                                                                                                                                                    = if Is_a(Mar, if _x_39 then _x_33 else _x_37) then 3
                                                                                                                                                      else
                                                                                                                                                      if Is_a(Jun,
                                                                                                                                                         if _x_39 then if _x_32 then Mar else …
                                                                                                                                                         else if _x_36 then Mar else …)
                                                                                                                                                      then 6 else if Is_a(Sep, if _x_39 then … else …) then 9 else 12
                                                                                                                                                in
                                                                                                                                                let (_x_41 : int) = ….leg_mult in
                                                                                                                                                let (_x_42 : int) = ….leg_mult in
                                                                                                                                                let (_x_43 : int) = ( :var_1: ).leg3.leg_mult in
                                                                                                                                                let (_x_44 : int)
                                                                                                                                                    = (if 0 <= _x_41 then _x_41 else -1 * _x_41)
                                                                                                                                                      + (if 0 <= _x_42 then _x_42 else -1 * _x_42)
                                                                                                                                                      + (if 0 <= _x_43 then _x_43 else -1 * _x_43)
                                                                                                                                                in
                                                                                                                                                ((_x_0 <= _x_1 || not (_x_11 <= _x_21)) || not (_x_25 <= _x_29))
                                                                                                                                                || not
                                                                                                                                                   (((_x_0 <= _x_30 || not (_x_40 <= _x_21)) || not (_x_25 <= _x_44))
                                                                                                                                                    && ((_x_30 <= _x_1 || not (_x_11 <= _x_40)) || not (_x_44 <= _x_29)))
                                                                                                                                                expansions
                                                                                                                                                []
                                                                                                                                                rewrite_steps
                                                                                                                                                  forward_chaining
                                                                                                                                                  • Sat (Some let (s1 : strategy) = {time_created = 0; leg1 = {leg_sec_idx = OUT1; leg_mult = 0}; leg2 = {leg_sec_idx = OUT3; leg_mult = 1}; leg3 = {leg_sec_idx = OUT1; leg_mult = 0}} let (s2 : strategy) = {time_created = (-2998); leg1 = {leg_sec_idx = OUT3; leg_mult = 0}; leg2 = {leg_sec_idx = OUT1; leg_mult = 0}; leg3 = {leg_sec_idx = OUT1; leg_mult = 0}} let (s3 : strategy) = {time_created = (-1); leg1 = {leg_sec_idx = OUT1; leg_mult = 0}; leg2 = {leg_sec_idx = OUT2; leg_mult = 0}; leg3 = {leg_sec_idx = OUT1; leg_mult = (-1)}} )

                                                                                                                                                  Ooops! It seems that our ranking criteria is not transitive. Let's check the results (note that the counter examples are now reflected into the run time in the CX module)

                                                                                                                                                  In [13]:
                                                                                                                                                  priority_strat CX.s1 CX.s2
                                                                                                                                                  
                                                                                                                                                  Out[13]:
                                                                                                                                                  - : bool = true
                                                                                                                                                  
                                                                                                                                                  In [14]:
                                                                                                                                                  priority_strat CX.s2 CX.s3
                                                                                                                                                  
                                                                                                                                                  Out[14]:
                                                                                                                                                  - : bool = true
                                                                                                                                                  
                                                                                                                                                  In [15]:
                                                                                                                                                  priority_strat CX.s1 CX.s3
                                                                                                                                                  
                                                                                                                                                  Out[15]:
                                                                                                                                                  - : bool = false
                                                                                                                                                  

                                                                                                                                                  3.2 Implied strategy price calculation

                                                                                                                                                  In [16]:
                                                                                                                                                  (* return the sum of volume at the highest level *)
                                                                                                                                                  let rec get_level_sums (orders : order list) (li : level_info option) =
                                                                                                                                                    match orders with
                                                                                                                                                    | [] -> li
                                                                                                                                                    | x::xs ->
                                                                                                                                                      begin
                                                                                                                                                        match li with
                                                                                                                                                        | None -> get_level_sums xs (Some {li_qty = x.o_qty; li_price = x.o_price})
                                                                                                                                                        | Some l ->
                                                                                                                                                          if (l.li_price = x.o_price) then
                                                                                                                                                            get_level_sums xs (Some {l with li_qty = l.li_qty + x.o_qty})
                                                                                                                                                          else
                                                                                                                                                            li
                                                                                                                                                      end
                                                                                                                                                  
                                                                                                                                                  (* Return best bid/ask levels *)
                                                                                                                                                  let get_book_tops (b : book) =
                                                                                                                                                    let bid_info = get_level_sums b.b_buys None in
                                                                                                                                                    let ask_info = get_level_sums b.b_sells None in
                                                                                                                                                    { bid_info; ask_info }
                                                                                                                                                  ;;
                                                                                                                                                  
                                                                                                                                                  (* Get the maximum number of strategy units here *)
                                                                                                                                                  (* Note that the units may have different signs, so we
                                                                                                                                                   need to make sure that we have enough *)
                                                                                                                                                  let calc_implied_strat_order (sid : strategy_id) (s : strategy) (books : books_info) (si : side) (time : int) =
                                                                                                                                                    let abs x = if x < 0 then -x else x in
                                                                                                                                                  
                                                                                                                                                    let adjust (mult : int) =
                                                                                                                                                      if si = BUY then mult else -mult in
                                                                                                                                                  
                                                                                                                                                    (* *)
                                                                                                                                                    let calc_max_out_mult (mult : int) (book : best_bid_ask)  =
                                                                                                                                                      if mult = 0 then
                                                                                                                                                        None
                                                                                                                                                      else
                                                                                                                                                        begin
                                                                                                                                                         if (adjust mult) > 0 then
                                                                                                                                                          match books.book1.bid_info with
                                                                                                                                                             | Some x -> Some (x.li_qty / (abs mult))
                                                                                                                                                             | None -> None
                                                                                                                                                         else
                                                                                                                                                             match book.ask_info with
                                                                                                                                                             | Some x -> Some (x.li_qty / (abs mult))
                                                                                                                                                             | None -> None
                                                                                                                                                        end in
                                                                                                                                                  
                                                                                                                                                    let mult1 = calc_max_out_mult s.leg1.leg_mult books.book1 in
                                                                                                                                                    let mult2 = calc_max_out_mult s.leg2.leg_mult books.book2 in
                                                                                                                                                    let mult3 = calc_max_out_mult s.leg3.leg_mult books.book3 in
                                                                                                                                                  
                                                                                                                                                    (* Compute the quantity *)
                                                                                                                                                    let max_strat =
                                                                                                                                                      begin
                                                                                                                                                         match mult1 with
                                                                                                                                                         | None -> 0
                                                                                                                                                         | Some x -> x
                                                                                                                                                      end in
                                                                                                                                                    let max_strat =
                                                                                                                                                      begin
                                                                                                                                                         match mult2 with
                                                                                                                                                         | None -> max_strat
                                                                                                                                                         | Some x -> if x < max_strat then x else max_strat
                                                                                                                                                      end in
                                                                                                                                                    let max_strat =
                                                                                                                                                      begin
                                                                                                                                                       match mult3 with
                                                                                                                                                       | None -> max_strat
                                                                                                                                                       | Some x -> if x < max_strat then x else max_strat
                                                                                                                                                      end in
                                                                                                                                                  
                                                                                                                                                    (* Now compute the price *)
                                                                                                                                                    let strat_price =
                                                                                                                                                      begin
                                                                                                                                                         match mult1 with
                                                                                                                                                         | None -> 0
                                                                                                                                                         | Some x ->
                                                                                                                                                           begin
                                                                                                                                                              if (adjust s.leg1.leg_mult) > 0 then
                                                                                                                                                                  match books.book1.bid_info with
                                                                                                                                                                  | Some x -> x.li_price * (adjust s.leg1.leg_mult)
                                                                                                                                                                  | None -> 0
                                                                                                                                                              else
                                                                                                                                                                  match books.book1.ask_info with
                                                                                                                                                                  | Some x -> x.li_price * (adjust s.leg1.leg_mult)
                                                                                                                                                                  | None -> 0
                                                                                                                                                           end
                                                                                                                                                      end in
                                                                                                                                                    let strat_price =
                                                                                                                                                      begin
                                                                                                                                                         match mult2 with
                                                                                                                                                         | None -> strat_price
                                                                                                                                                         | Some x ->
                                                                                                                                                           begin
                                                                                                                                                              if (adjust s.leg2.leg_mult) > 0 then
                                                                                                                                                                  match books.book2.bid_info with
                                                                                                                                                                  | Some x -> x.li_price * (adjust s.leg2.leg_mult) + strat_price
                                                                                                                                                                  | None -> strat_price
                                                                                                                                                              else
                                                                                                                                                                  match books.book2.ask_info with
                                                                                                                                                                  | Some x -> x.li_price * (adjust s.leg2.leg_mult) + strat_price
                                                                                                                                                                  | None -> strat_price
                                                                                                                                                           end
                                                                                                                                                      end in
                                                                                                                                                    let strat_price =
                                                                                                                                                      begin
                                                                                                                                                         match mult3 with
                                                                                                                                                         | None -> strat_price
                                                                                                                                                         | Some x ->
                                                                                                                                                           begin
                                                                                                                                                              if (adjust s.leg3.leg_mult) > 0 then
                                                                                                                                                                  match books.book3.bid_info with
                                                                                                                                                                  | Some x -> x.li_price * (adjust s.leg3.leg_mult) + strat_price
                                                                                                                                                                  | None -> strat_price
                                                                                                                                                              else
                                                                                                                                                                  match books.book3.ask_info with
                                                                                                                                                                  | Some x -> x.li_price * (adjust s.leg3.leg_mult) + strat_price
                                                                                                                                                                  | None -> strat_price
                                                                                                                                                           end
                                                                                                                                                      end in
                                                                                                                                                  
                                                                                                                                                    (* Now form the new implied order here... *)
                                                                                                                                                    {
                                                                                                                                                     o_qty = max_strat
                                                                                                                                                     ; o_price = strat_price
                                                                                                                                                     ; o_id = -1
                                                                                                                                                     ; o_time = time
                                                                                                                                                     ; o_side = si
                                                                                                                                                     ; o_client_id = -1
                                                                                                                                                     ; o_inst = Strategy sid
                                                                                                                                                     ; o_is_implied = true }
                                                                                                                                                  ;;
                                                                                                                                                  
                                                                                                                                                  Out[16]:
                                                                                                                                                  val get_level_sums : order list -> level_info option -> level_info option =
                                                                                                                                                    <fun>
                                                                                                                                                  val get_book_tops : book -> best_bid_ask = <fun>
                                                                                                                                                  val calc_implied_strat_order :
                                                                                                                                                    strategy_id -> strategy -> books_info -> side -> int -> order = <fun>
                                                                                                                                                  
                                                                                                                                                  termination proof

                                                                                                                                                  Termination proof

                                                                                                                                                  call `let (_x_0 : order) = List.hd orders in get_level_sums (List.tl orders) (Some {li_qty = _x_0.o_qty; li_price = _x_0.o_price})` from `get_level_sums orders li`
                                                                                                                                                  originalget_level_sums orders li
                                                                                                                                                  sublet (_x_0 : order) = List.hd orders in get_level_sums (List.tl orders) (Some {li_qty = _x_0.o_qty; li_price = _x_0.o_price})
                                                                                                                                                  original ordinalOrdinal.Int (_cnt orders)
                                                                                                                                                  sub ordinalOrdinal.Int (_cnt (List.tl orders))
                                                                                                                                                  path[Is_a(None, li) && not Is_a([], orders)]
                                                                                                                                                  proof
                                                                                                                                                  detailed proof
                                                                                                                                                  ground_instances3
                                                                                                                                                  definitions0
                                                                                                                                                  inductions0
                                                                                                                                                  search_time
                                                                                                                                                  0.021s
                                                                                                                                                  details
                                                                                                                                                  Expand
                                                                                                                                                  smt_stats
                                                                                                                                                  num checks8
                                                                                                                                                  arith-assume-eqs9
                                                                                                                                                  arith-make-feasible70
                                                                                                                                                  arith-max-columns50
                                                                                                                                                  arith-conflicts2
                                                                                                                                                  rlimit count9733
                                                                                                                                                  mk clause102
                                                                                                                                                  datatype occurs check47
                                                                                                                                                  mk bool var274
                                                                                                                                                  arith-lower39
                                                                                                                                                  datatype splits39
                                                                                                                                                  decisions69
                                                                                                                                                  propagations68
                                                                                                                                                  interface eqs9
                                                                                                                                                  arith-max-rows22
                                                                                                                                                  conflicts6
                                                                                                                                                  datatype accessor ax30
                                                                                                                                                  datatype constructor ax58
                                                                                                                                                  num allocs1560829550
                                                                                                                                                  final checks15
                                                                                                                                                  added eqs306
                                                                                                                                                  del clause73
                                                                                                                                                  arith eq adapter37
                                                                                                                                                  arith-upper64
                                                                                                                                                  memory31.380000
                                                                                                                                                  max memory78.250000
                                                                                                                                                  Expand
                                                                                                                                                  • start[0.021s]
                                                                                                                                                      let (_x_0 : int) = count.list count.order orders in
                                                                                                                                                      let (_x_1 : order list) = List.tl orders in
                                                                                                                                                      let (_x_2 : int) = count.list count.order _x_1 in
                                                                                                                                                      Is_a(None, li) && not Is_a([], orders) && _x_0 >= 0 && _x_2 >= 0
                                                                                                                                                      ==> not
                                                                                                                                                          ((List.hd orders).o_price = (List.hd _x_1).o_price
                                                                                                                                                           && not Is_a([], _x_1))
                                                                                                                                                          || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                                                  • simplify
                                                                                                                                                    into
                                                                                                                                                    let (_x_0 : order list) = List.tl orders in
                                                                                                                                                    let (_x_1 : int) = count.list count.order _x_0 in
                                                                                                                                                    let (_x_2 : int) = count.list count.order orders in
                                                                                                                                                    (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                                                                                                     || not
                                                                                                                                                        ((List.hd orders).o_price = (List.hd _x_0).o_price && not Is_a([], _x_0)))
                                                                                                                                                    || not (((Is_a(None, li) && not Is_a([], orders)) && _x_2 >= 0) && _x_1 >= 0)
                                                                                                                                                    expansions
                                                                                                                                                    []
                                                                                                                                                    rewrite_steps
                                                                                                                                                      forward_chaining
                                                                                                                                                      • unroll
                                                                                                                                                        expr
                                                                                                                                                        (|`count.list count.order[0]`_3745| orders_3730)
                                                                                                                                                        expansions
                                                                                                                                                        • unroll
                                                                                                                                                          expr
                                                                                                                                                          (|`count.list count.order[0]`_3745| (|get.::.1_3726| orders_3730))
                                                                                                                                                          expansions
                                                                                                                                                          • unroll
                                                                                                                                                            expr
                                                                                                                                                            (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                                                                                (|`count.list count.order[0]`_3745|
                                                                                                                                                                   …
                                                                                                                                                            expansions
                                                                                                                                                            • Unsat

                                                                                                                                                            call `let (_x_0 : level_info) = Option.get li in get_level_sums (List.tl orders) (Some {_x_0 with li_qty = _x_0.li_qty + (List.hd orders).o_qty})` from `get_level_sums orders li`
                                                                                                                                                            originalget_level_sums orders li
                                                                                                                                                            sublet (_x_0 : level_info) = Option.get li in get_level_sums (List.tl orders) (Some {_x_0 with li_qty = _x_0.li_qty + (List.hd orders).o_qty})
                                                                                                                                                            original ordinalOrdinal.Int (_cnt orders)
                                                                                                                                                            sub ordinalOrdinal.Int (_cnt (List.tl orders))
                                                                                                                                                            path[(Option.get li).li_price = (List.hd orders).o_price && not Is_a(None, li) && not Is_a([], orders)]
                                                                                                                                                            proof
                                                                                                                                                            detailed proof
                                                                                                                                                            ground_instances3
                                                                                                                                                            definitions0
                                                                                                                                                            inductions0
                                                                                                                                                            search_time
                                                                                                                                                            0.028s
                                                                                                                                                            details
                                                                                                                                                            Expand
                                                                                                                                                            smt_stats
                                                                                                                                                            num checks8
                                                                                                                                                            arith-assume-eqs14
                                                                                                                                                            arith-make-feasible71
                                                                                                                                                            arith-max-columns55
                                                                                                                                                            arith-conflicts2
                                                                                                                                                            rlimit count4934
                                                                                                                                                            mk clause116
                                                                                                                                                            datatype occurs check67
                                                                                                                                                            mk bool var283
                                                                                                                                                            arith-lower38
                                                                                                                                                            datatype splits39
                                                                                                                                                            decisions76
                                                                                                                                                            propagations62
                                                                                                                                                            interface eqs14
                                                                                                                                                            arith-max-rows27
                                                                                                                                                            conflicts6
                                                                                                                                                            datatype accessor ax31
                                                                                                                                                            datatype constructor ax59
                                                                                                                                                            num allocs1487133428
                                                                                                                                                            final checks20
                                                                                                                                                            added eqs311
                                                                                                                                                            del clause87
                                                                                                                                                            arith eq adapter36
                                                                                                                                                            arith-upper57
                                                                                                                                                            memory31.270000
                                                                                                                                                            max memory78.250000
                                                                                                                                                            Expand
                                                                                                                                                            • start[0.028s]
                                                                                                                                                                let (_x_0 : int) = (Option.get li).li_price in
                                                                                                                                                                let (_x_1 : int) = count.list count.order orders in
                                                                                                                                                                let (_x_2 : order list) = List.tl orders in
                                                                                                                                                                let (_x_3 : int) = count.list count.order _x_2 in
                                                                                                                                                                _x_0 = (List.hd orders).o_price
                                                                                                                                                                && not Is_a(None, li) && not Is_a([], orders) && _x_1 >= 0 && _x_3 >= 0
                                                                                                                                                                ==> not (_x_0 = (List.hd _x_2).o_price && not Is_a([], _x_2))
                                                                                                                                                                    || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_1)
                                                                                                                                                            • simplify
                                                                                                                                                              into
                                                                                                                                                              let (_x_0 : int) = (Option.get li).li_price in
                                                                                                                                                              let (_x_1 : order list) = List.tl orders in
                                                                                                                                                              let (_x_2 : int) = count.list count.order _x_1 in
                                                                                                                                                              let (_x_3 : int) = count.list count.order orders in
                                                                                                                                                              (not (_x_0 = (List.hd _x_1).o_price && not Is_a([], _x_1))
                                                                                                                                                               || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_3))
                                                                                                                                                              || not
                                                                                                                                                                 ((((_x_0 = (List.hd orders).o_price && not Is_a(None, li))
                                                                                                                                                                    && not Is_a([], orders))
                                                                                                                                                                   && _x_3 >= 0)
                                                                                                                                                                  && _x_2 >= 0)
                                                                                                                                                              expansions
                                                                                                                                                              []
                                                                                                                                                              rewrite_steps
                                                                                                                                                                forward_chaining
                                                                                                                                                                • unroll
                                                                                                                                                                  expr
                                                                                                                                                                  (|`count.list count.order[0]`_3745| orders_3730)
                                                                                                                                                                  expansions
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr
                                                                                                                                                                    (|`count.list count.order[0]`_3745| (|get.::.1_3726| orders_3730))
                                                                                                                                                                    expansions
                                                                                                                                                                    • unroll
                                                                                                                                                                      expr
                                                                                                                                                                      (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                                                                                          (|`count.list count.order[0]`_3745|
                                                                                                                                                                             …
                                                                                                                                                                      expansions
                                                                                                                                                                      • Unsat

                                                                                                                                                                      Let's now try to experiment with this.

                                                                                                                                                                      In [17]:
                                                                                                                                                                      let strat1 = {
                                                                                                                                                                        time_created = 1;
                                                                                                                                                                        leg1    = { leg_sec_idx = OUT1; leg_mult = 1 }
                                                                                                                                                                        ; leg2  = { leg_sec_idx = OUT2; leg_mult = 0 }
                                                                                                                                                                        ; leg3  = { leg_sec_idx = OUT3; leg_mult = 0 }
                                                                                                                                                                      };;
                                                                                                                                                                      
                                                                                                                                                                      let books = {
                                                                                                                                                                          book1 = { bid_info = None ; ask_info = Some { li_qty = 100 ; li_price = 450 }}
                                                                                                                                                                        ; book2 = { bid_info = Some { li_qty = 125 ; li_price = 100 }; ask_info = Some { li_qty = 100 ; li_price = 350 }}
                                                                                                                                                                        ; book3 = { bid_info = None ; ask_info = Some { li_qty = 100 ; li_price = 425 }}
                                                                                                                                                                      };;
                                                                                                                                                                      
                                                                                                                                                                      (* This should just replicate the OUT1 security on the SELL side *)
                                                                                                                                                                      calc_implied_strat_order STRAT1 strat1 books SELL 1
                                                                                                                                                                      
                                                                                                                                                                      Out[17]:
                                                                                                                                                                      val strat1 : strategy =
                                                                                                                                                                        {time_created = 1; leg1 = {leg_sec_idx = OUT1; leg_mult = 1};
                                                                                                                                                                         leg2 = {leg_sec_idx = OUT2; leg_mult = 0};
                                                                                                                                                                         leg3 = {leg_sec_idx = OUT3; leg_mult = 0}}
                                                                                                                                                                      val books : books_info =
                                                                                                                                                                        {book1 = {bid_info = None; ask_info = Some {li_qty = 100; li_price = 450}};
                                                                                                                                                                         book2 =
                                                                                                                                                                          {bid_info = Some {li_qty = 125; li_price = 100};
                                                                                                                                                                           ask_info = Some {li_qty = 100; li_price = 350}};
                                                                                                                                                                         book3 = {bid_info = None; ask_info = Some {li_qty = 100; li_price = 425}}}
                                                                                                                                                                      - : order =
                                                                                                                                                                      {o_qty = 100; o_price = -450; o_time = 1; o_id = -1; o_side = SELL;
                                                                                                                                                                       o_client_id = -1; o_inst = Strategy STRAT1; o_is_implied = true}
                                                                                                                                                                      
                                                                                                                                                                      In [18]:
                                                                                                                                                                      (* Now let's try the same on the BUY side - there should not be any available orders as the bid is empty *)
                                                                                                                                                                      calc_implied_strat_order STRAT1 strat1 books BUY 1
                                                                                                                                                                      
                                                                                                                                                                      Out[18]:
                                                                                                                                                                      - : order =
                                                                                                                                                                      {o_qty = 0; o_price = 0; o_time = 1; o_id = -1; o_side = BUY;
                                                                                                                                                                       o_client_id = -1; o_inst = Strategy STRAT1; o_is_implied = true}
                                                                                                                                                                      
                                                                                                                                                                      In [19]:
                                                                                                                                                                      (* let's try to mix up the legs now *)
                                                                                                                                                                      
                                                                                                                                                                      let strat2 = {
                                                                                                                                                                       strat1 with
                                                                                                                                                                       leg2 = {leg_sec_idx = OUT2; leg_mult = -1}
                                                                                                                                                                      };;
                                                                                                                                                                      
                                                                                                                                                                      (* This will not result in any orders because there's no BUY *)
                                                                                                                                                                      calc_implied_strat_order STRAT1 strat2 books BUY 1
                                                                                                                                                                      
                                                                                                                                                                      Out[19]:
                                                                                                                                                                      val strat2 : strategy =
                                                                                                                                                                        {time_created = 1; leg1 = {leg_sec_idx = OUT1; leg_mult = 1};
                                                                                                                                                                         leg2 = {leg_sec_idx = OUT2; leg_mult = -1};
                                                                                                                                                                         leg3 = {leg_sec_idx = OUT3; leg_mult = 0}}
                                                                                                                                                                      - : order =
                                                                                                                                                                      {o_qty = 0; o_price = -350; o_time = 1; o_id = -1; o_side = BUY;
                                                                                                                                                                       o_client_id = -1; o_inst = Strategy STRAT1; o_is_implied = true}
                                                                                                                                                                      
                                                                                                                                                                      In [20]:
                                                                                                                                                                      calc_implied_strat_order STRAT2 strat2 books SELL 1
                                                                                                                                                                      
                                                                                                                                                                      Out[20]:
                                                                                                                                                                      - : order =
                                                                                                                                                                      {o_qty = 100; o_price = -450; o_time = 1; o_id = -1; o_side = SELL;
                                                                                                                                                                       o_client_id = -1; o_inst = Strategy STRAT2; o_is_implied = true}
                                                                                                                                                                      
                                                                                                                                                                      In [21]:
                                                                                                                                                                      let strat = {
                                                                                                                                                                        time_created = 1;
                                                                                                                                                                        leg1    = { leg_sec_idx = OUT1; leg_mult = 1 }
                                                                                                                                                                        ; leg2  = { leg_sec_idx = OUT2; leg_mult = -2 }
                                                                                                                                                                        ; leg3  = { leg_sec_idx = OUT3; leg_mult = 0 }
                                                                                                                                                                      };;
                                                                                                                                                                      
                                                                                                                                                                      let books = {
                                                                                                                                                                          book1 = { bid_info = Some { li_qty = 500; li_price = 50 } ; ask_info = Some { li_qty = 750 ; li_price = 50 }}
                                                                                                                                                                        ; book2 = { bid_info = Some { li_qty = 200 ; li_price = 60 }; ask_info = Some { li_qty = 500 ; li_price = 70 }}
                                                                                                                                                                        ; book3 = { bid_info = None ; ask_info = None }
                                                                                                                                                                      };;
                                                                                                                                                                      
                                                                                                                                                                      calc_implied_strat_order STRAT1 strat books BUY 1
                                                                                                                                                                      
                                                                                                                                                                      Out[21]:
                                                                                                                                                                      val strat : strategy =
                                                                                                                                                                        {time_created = 1; leg1 = {leg_sec_idx = OUT1; leg_mult = 1};
                                                                                                                                                                         leg2 = {leg_sec_idx = OUT2; leg_mult = -2};
                                                                                                                                                                         leg3 = {leg_sec_idx = OUT3; leg_mult = 0}}
                                                                                                                                                                      val books : books_info =
                                                                                                                                                                        {book1 =
                                                                                                                                                                          {bid_info = Some {li_qty = 500; li_price = 50};
                                                                                                                                                                           ask_info = Some {li_qty = 750; li_price = 50}};
                                                                                                                                                                         book2 =
                                                                                                                                                                          {bid_info = Some {li_qty = 200; li_price = 60};
                                                                                                                                                                           ask_info = Some {li_qty = 500; li_price = 70}};
                                                                                                                                                                         book3 = {bid_info = None; ask_info = None}}
                                                                                                                                                                      - : order =
                                                                                                                                                                      {o_qty = 250; o_price = -90; o_time = 1; o_id = -1; o_side = BUY;
                                                                                                                                                                       o_client_id = -1; o_inst = Strategy STRAT1; o_is_implied = true}
                                                                                                                                                                      

                                                                                                                                                                      3.3 Implied uncrossing operations

                                                                                                                                                                      In [22]:
                                                                                                                                                                      (* removes implied orders from a book *)
                                                                                                                                                                      let remove_imp_orders (b : book) =
                                                                                                                                                                        let rec remove_imp_orders_side (orders : order list) =
                                                                                                                                                                          match orders with
                                                                                                                                                                          | [] -> []
                                                                                                                                                                          | x::xs ->
                                                                                                                                                                              if x.o_is_implied then
                                                                                                                                                                                (remove_imp_orders_side xs)
                                                                                                                                                                              else
                                                                                                                                                                                x::(remove_imp_orders_side xs) in
                                                                                                                                                                      
                                                                                                                                                                        { b_buys = (remove_imp_orders_side b.b_buys)
                                                                                                                                                                        ; b_sells = (remove_imp_orders_side b.b_sells)
                                                                                                                                                                        }
                                                                                                                                                                      
                                                                                                                                                                      (* Allocate implied fills to the book and return fills *)
                                                                                                                                                                      let allocate_implied_fills (b : book) (qty : int) (price : int) (time : int) =
                                                                                                                                                                        if qty = 0 then {
                                                                                                                                                                          uncrossed_book = b
                                                                                                                                                                          ; uncrossed_fills = []
                                                                                                                                                                          ; uncrossed_qty = 0
                                                                                                                                                                        } else
                                                                                                                                                                        begin
                                                                                                                                                                          (* Insert new order into the book and uncross it *)
                                                                                                                                                                          let new_order = {
                                                                                                                                                                            o_qty = if qty < 0 then (-qty) else qty
                                                                                                                                                                            ; o_price = price
                                                                                                                                                                            ; o_id = -1
                                                                                                                                                                            ; o_time = time
                                                                                                                                                                            ; o_side = if qty < 0 then SELL else BUY
                                                                                                                                                                            ; o_client_id = -1
                                                                                                                                                                            ; o_inst = Outright OUT1
                                                                                                                                                                            ; o_is_implied = true
                                                                                                                                                                          } in
                                                                                                                                                                      
                                                                                                                                                                          (* create new order that we will trade *)
                                                                                                                                                                          let b' = insert_order new_order b in
                                                                                                                                                                      
                                                                                                                                                                          (* finally we will uncross the book and return results *)
                                                                                                                                                                          (uncross_book b' [] 0)
                                                                                                                                                                        end
                                                                                                                                                                      
                                                                                                                                                                      (* Calculate the price at which implied orders should trade in the outright books *)
                                                                                                                                                                      let calc_implied_trade_price (mult : int) (bidask : best_bid_ask) =
                                                                                                                                                                        if mult > 0 then
                                                                                                                                                                         begin
                                                                                                                                                                          match bidask.ask_info with
                                                                                                                                                                            | None -> 0
                                                                                                                                                                            | Some x -> x.li_price
                                                                                                                                                                          end
                                                                                                                                                                        else
                                                                                                                                                                          begin
                                                                                                                                                                              match bidask.bid_info with
                                                                                                                                                                                | None -> 0
                                                                                                                                                                                | Some x -> x.li_price
                                                                                                                                                                          end
                                                                                                                                                                      ;;
                                                                                                                                                                      
                                                                                                                                                                      Out[22]:
                                                                                                                                                                      val remove_imp_orders : book -> book = <fun>
                                                                                                                                                                      val allocate_implied_fills : book -> int -> int -> int -> uncross_res = <fun>
                                                                                                                                                                      val calc_implied_trade_price : int -> best_bid_ask -> int = <fun>
                                                                                                                                                                      
                                                                                                                                                                      termination proof

                                                                                                                                                                      Termination proof

                                                                                                                                                                      call `recfun.remove_imp_orders.remove_imp_orders_side.0 (List.tl orders)` from `recfun.remove_imp_orders.remove_imp_orders_side.0 orders`
                                                                                                                                                                      originalrecfun.remove_imp_orders.remove_imp_orders_side.0 orders
                                                                                                                                                                      subrecfun.remove_imp_orders.remove_imp_orders_side.0 (List.tl orders)
                                                                                                                                                                      original ordinalOrdinal.Int (_cnt orders)
                                                                                                                                                                      sub ordinalOrdinal.Int (_cnt (List.tl orders))
                                                                                                                                                                      path[(List.hd orders).o_is_implied && not Is_a([], orders)]
                                                                                                                                                                      proof
                                                                                                                                                                      detailed proof
                                                                                                                                                                      ground_instances3
                                                                                                                                                                      definitions0
                                                                                                                                                                      inductions0
                                                                                                                                                                      search_time
                                                                                                                                                                      0.027s
                                                                                                                                                                      details
                                                                                                                                                                      Expand
                                                                                                                                                                      smt_stats
                                                                                                                                                                      num checks8
                                                                                                                                                                      arith-assume-eqs15
                                                                                                                                                                      arith-make-feasible76
                                                                                                                                                                      arith-max-columns60
                                                                                                                                                                      arith-conflicts2
                                                                                                                                                                      rlimit count10122
                                                                                                                                                                      mk clause135
                                                                                                                                                                      datatype occurs check54
                                                                                                                                                                      mk bool var302
                                                                                                                                                                      arith-lower44
                                                                                                                                                                      datatype splits39
                                                                                                                                                                      decisions77
                                                                                                                                                                      propagations88
                                                                                                                                                                      interface eqs15
                                                                                                                                                                      arith-max-rows30
                                                                                                                                                                      conflicts7
                                                                                                                                                                      datatype accessor ax31
                                                                                                                                                                      datatype constructor ax59
                                                                                                                                                                      num allocs1656866205
                                                                                                                                                                      final checks21
                                                                                                                                                                      added eqs322
                                                                                                                                                                      del clause101
                                                                                                                                                                      arith eq adapter42
                                                                                                                                                                      arith-upper68
                                                                                                                                                                      memory38.380000
                                                                                                                                                                      max memory78.250000
                                                                                                                                                                      Expand
                                                                                                                                                                      • start[0.027s]
                                                                                                                                                                          let (_x_0 : int) = count.list count.order orders in
                                                                                                                                                                          let (_x_1 : order list) = List.tl orders in
                                                                                                                                                                          let (_x_2 : int) = count.list count.order _x_1 in
                                                                                                                                                                          let (_x_3 : bool) = (List.hd _x_1).o_is_implied in
                                                                                                                                                                          let (_x_4 : bool) = not Is_a([], _x_1) in
                                                                                                                                                                          (List.hd orders).o_is_implied
                                                                                                                                                                          && not Is_a([], orders) && _x_0 >= 0 && _x_2 >= 0
                                                                                                                                                                          ==> not (_x_3 && _x_4) && not (not _x_3 && _x_4)
                                                                                                                                                                              || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                                                                      • simplify
                                                                                                                                                                        into
                                                                                                                                                                        let (_x_0 : order list) = List.tl orders in
                                                                                                                                                                        let (_x_1 : bool) = (List.hd _x_0).o_is_implied in
                                                                                                                                                                        let (_x_2 : bool) = not Is_a([], _x_0) in
                                                                                                                                                                        let (_x_3 : int) = count.list count.order _x_0 in
                                                                                                                                                                        let (_x_4 : int) = count.list count.order orders in
                                                                                                                                                                        (not (_x_1 && _x_2) && not (not _x_1 && _x_2)
                                                                                                                                                                         || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4))
                                                                                                                                                                        || not
                                                                                                                                                                           ((((List.hd orders).o_is_implied && not Is_a([], orders)) && _x_4 >= 0)
                                                                                                                                                                            && _x_3 >= 0)
                                                                                                                                                                        expansions
                                                                                                                                                                        []
                                                                                                                                                                        rewrite_steps
                                                                                                                                                                          forward_chaining
                                                                                                                                                                          • unroll
                                                                                                                                                                            expr
                                                                                                                                                                            (|`count.list count.order[0]`_3891| orders_3878)
                                                                                                                                                                            expansions
                                                                                                                                                                            • unroll
                                                                                                                                                                              expr
                                                                                                                                                                              (|`count.list count.order[0]`_3891| (|get.::.1_3876| orders_3878))
                                                                                                                                                                              expansions
                                                                                                                                                                              • unroll
                                                                                                                                                                                expr
                                                                                                                                                                                (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                                                                                                    (|`count.list count.order[0]`_3891|
                                                                                                                                                                                       …
                                                                                                                                                                                expansions
                                                                                                                                                                                • Unsat

                                                                                                                                                                                call `recfun.remove_imp_orders.remove_imp_orders_side.0 (List.tl orders)` from `recfun.remove_imp_orders.remove_imp_orders_side.0 orders`
                                                                                                                                                                                originalrecfun.remove_imp_orders.remove_imp_orders_side.0 orders
                                                                                                                                                                                subrecfun.remove_imp_orders.remove_imp_orders_side.0 (List.tl orders)
                                                                                                                                                                                original ordinalOrdinal.Int (_cnt orders)
                                                                                                                                                                                sub ordinalOrdinal.Int (_cnt (List.tl orders))
                                                                                                                                                                                path[not (List.hd orders).o_is_implied && not Is_a([], orders)]
                                                                                                                                                                                proof
                                                                                                                                                                                detailed proof
                                                                                                                                                                                ground_instances3
                                                                                                                                                                                definitions0
                                                                                                                                                                                inductions0
                                                                                                                                                                                search_time
                                                                                                                                                                                0.019s
                                                                                                                                                                                details
                                                                                                                                                                                Expand
                                                                                                                                                                                smt_stats
                                                                                                                                                                                num checks8
                                                                                                                                                                                arith-assume-eqs15
                                                                                                                                                                                arith-make-feasible87
                                                                                                                                                                                arith-max-columns60
                                                                                                                                                                                arith-conflicts2
                                                                                                                                                                                rlimit count5192
                                                                                                                                                                                mk clause141
                                                                                                                                                                                datatype occurs check54
                                                                                                                                                                                mk bool var316
                                                                                                                                                                                arith-lower50
                                                                                                                                                                                datatype splits39
                                                                                                                                                                                decisions86
                                                                                                                                                                                propagations99
                                                                                                                                                                                interface eqs15
                                                                                                                                                                                arith-max-rows30
                                                                                                                                                                                conflicts7
                                                                                                                                                                                datatype accessor ax32
                                                                                                                                                                                datatype constructor ax61
                                                                                                                                                                                num allocs1617990163
                                                                                                                                                                                final checks21
                                                                                                                                                                                added eqs340
                                                                                                                                                                                del clause107
                                                                                                                                                                                arith eq adapter48
                                                                                                                                                                                arith-upper80
                                                                                                                                                                                memory35.550000
                                                                                                                                                                                max memory78.250000
                                                                                                                                                                                Expand
                                                                                                                                                                                • start[0.019s]
                                                                                                                                                                                    let (_x_0 : int) = count.list count.order orders in
                                                                                                                                                                                    let (_x_1 : order list) = List.tl orders in
                                                                                                                                                                                    let (_x_2 : int) = count.list count.order _x_1 in
                                                                                                                                                                                    let (_x_3 : bool) = (List.hd _x_1).o_is_implied in
                                                                                                                                                                                    let (_x_4 : bool) = not Is_a([], _x_1) in
                                                                                                                                                                                    not (List.hd orders).o_is_implied
                                                                                                                                                                                    && not Is_a([], orders) && _x_0 >= 0 && _x_2 >= 0
                                                                                                                                                                                    ==> not (_x_3 && _x_4) && not (not _x_3 && _x_4)
                                                                                                                                                                                        || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                                                                                • simplify
                                                                                                                                                                                  into
                                                                                                                                                                                  let (_x_0 : order list) = List.tl orders in
                                                                                                                                                                                  let (_x_1 : bool) = (List.hd _x_0).o_is_implied in
                                                                                                                                                                                  let (_x_2 : bool) = not Is_a([], _x_0) in
                                                                                                                                                                                  let (_x_3 : int) = count.list count.order _x_0 in
                                                                                                                                                                                  let (_x_4 : int) = count.list count.order orders in
                                                                                                                                                                                  (not (_x_1 && _x_2) && not (not _x_1 && _x_2)
                                                                                                                                                                                   || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4))
                                                                                                                                                                                  || not
                                                                                                                                                                                     (((not (List.hd orders).o_is_implied && not Is_a([], orders)) && _x_4 >= 0)
                                                                                                                                                                                      && _x_3 >= 0)
                                                                                                                                                                                  expansions
                                                                                                                                                                                  []
                                                                                                                                                                                  rewrite_steps
                                                                                                                                                                                    forward_chaining
                                                                                                                                                                                    • unroll
                                                                                                                                                                                      expr
                                                                                                                                                                                      (|`count.list count.order[0]`_3891| orders_3878)
                                                                                                                                                                                      expansions
                                                                                                                                                                                      • unroll
                                                                                                                                                                                        expr
                                                                                                                                                                                        (|`count.list count.order[0]`_3891| (|get.::.1_3876| orders_3878))
                                                                                                                                                                                        expansions
                                                                                                                                                                                        • unroll
                                                                                                                                                                                          expr
                                                                                                                                                                                          (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                                                                                                                              (|`count.list count.order[0]`_3891|
                                                                                                                                                                                                 …
                                                                                                                                                                                          expansions
                                                                                                                                                                                          • Unsat

                                                                                                                                                                                          3.4 Implied uncrossing (for single side)

                                                                                                                                                                                          In [23]:
                                                                                                                                                                                          (* The actual cycle *)
                                                                                                                                                                                          let implied_uncross_side (sd : side) (s_id : strategy_id) (s : strategy) (m : market) =
                                                                                                                                                                                          
                                                                                                                                                                                            (* 0. get the top of the book s*)
                                                                                                                                                                                            let book1 = get_book_tops m.out_book1 in
                                                                                                                                                                                            let book2 = get_book_tops m.out_book2 in
                                                                                                                                                                                            let book3 = get_book_tops m.out_book3 in
                                                                                                                                                                                          
                                                                                                                                                                                            let books_tops = { book1; book2; book3 } in
                                                                                                                                                                                          
                                                                                                                                                                                            (* 1. calculate the implied orders that are available right now... *)
                                                                                                                                                                                            let imp_order = calc_implied_strat_order s_id s books_tops sd m.curr_time in
                                                                                                                                                                                          
                                                                                                                                                                                            (* Need to increase the order ID first *)
                                                                                                                                                                                            let new_ord_id = m.last_ord_id + 1 in
                                                                                                                                                                                          
                                                                                                                                                                                            (* 2. insert them into the order book *)
                                                                                                                                                                                            let strat_book =
                                                                                                                                                                                              begin
                                                                                                                                                                                                match s_id with
                                                                                                                                                                                                | STRAT1 -> insert_order { imp_order with o_id = new_ord_id } m.s_book1
                                                                                                                                                                                                | STRAT2 -> insert_order { imp_order with o_id = new_ord_id } m.s_book2
                                                                                                                                                                                              end in
                                                                                                                                                                                          
                                                                                                                                                                                            (* 3. perform the uncross - get the fills, etc... *)
                                                                                                                                                                                            let unc_result = uncross_book strat_book [] 0 in
                                                                                                                                                                                          
                                                                                                                                                                                            let fq = unc_result.uncrossed_qty in
                                                                                                                                                                                          
                                                                                                                                                                                            if fq = 0 then
                                                                                                                                                                                              (* Since we didn't trade anything, let's just return the original market state *)
                                                                                                                                                                                              m
                                                                                                                                                                                            else
                                                                                                                                                                                          
                                                                                                                                                                                            let adjust (mult : int) =
                                                                                                                                                                                              let mult = -mult in
                                                                                                                                                                                              if sd = BUY then mult else -mult in
                                                                                                                                                                                          
                                                                                                                                                                                            let adj_mul1 = adjust s.leg1.leg_mult in
                                                                                                                                                                                            let adj_mul2 = adjust s.leg2.leg_mult in
                                                                                                                                                                                            let adj_mul3 = adjust s.leg3.leg_mult in
                                                                                                                                                                                          
                                                                                                                                                                                            (* calculate the prices at which outright orders will trade *)
                                                                                                                                                                                            let price1 = calc_implied_trade_price adj_mul1 book1 in
                                                                                                                                                                                            let price2 = calc_implied_trade_price adj_mul2 book2 in
                                                                                                                                                                                            let price3 = calc_implied_trade_price adj_mul3 book3 in
                                                                                                                                                                                          
                                                                                                                                                                                            (* 4. allocate fills to the outright orders *)
                                                                                                                                                                                            let out_book1_res = allocate_implied_fills m.out_book1 (fq * adj_mul1) price1 m.curr_time in
                                                                                                                                                                                            let out_book2_res = allocate_implied_fills m.out_book2 (fq * adj_mul2) price2 m.curr_time in
                                                                                                                                                                                            let out_book3_res = allocate_implied_fills m.out_book3 (fq * adj_mul3) price3 m.curr_time in
                                                                                                                                                                                          
                                                                                                                                                                                            (* 5. remove the implied orders - notice that the uncrossed result contains a new book
                                                                                                                                                                                              with partial fills *)
                                                                                                                                                                                            let m = match s_id with
                                                                                                                                                                                            | STRAT1 -> { m with s_book1 = remove_imp_orders unc_result.uncrossed_book }
                                                                                                                                                                                            | STRAT2 -> { m with s_book2 = remove_imp_orders unc_result.uncrossed_book } in
                                                                                                                                                                                          
                                                                                                                                                                                            (* 6. let's now gather all of the fills and turn them into outbound messages *)
                                                                                                                                                                                            let new_fill_msgs = create_fill_msgs (unc_result.uncrossed_fills @ out_book1_res.uncrossed_fills
                                                                                                                                                                                              @ out_book2_res.uncrossed_fills @ out_book3_res.uncrossed_fills) in
                                                                                                                                                                                          
                                                                                                                                                                                            { m with
                                                                                                                                                                                              outbound_msgs = new_fill_msgs @ m.outbound_msgs
                                                                                                                                                                                              ; out_book1 = out_book1_res.uncrossed_book
                                                                                                                                                                                              ; out_book2 = out_book2_res.uncrossed_book
                                                                                                                                                                                              ; out_book3 = out_book3_res.uncrossed_book
                                                                                                                                                                                              ; last_ord_id = new_ord_id }
                                                                                                                                                                                          ;;
                                                                                                                                                                                          
                                                                                                                                                                                          Out[23]:
                                                                                                                                                                                          val implied_uncross_side :
                                                                                                                                                                                            side -> strategy_id -> strategy -> market -> market = <fun>
                                                                                                                                                                                          

                                                                                                                                                                                          Let's now experiment with some concrete examples.

                                                                                                                                                                                          In [24]:
                                                                                                                                                                                          #program;;
                                                                                                                                                                                          (* #remove_doc doc_of_market;; *)
                                                                                                                                                                                          #logic;;
                                                                                                                                                                                          
                                                                                                                                                                                          let strat = {
                                                                                                                                                                                            time_created = 1;
                                                                                                                                                                                            leg1    = { leg_sec_idx = OUT1; leg_mult = 1 }
                                                                                                                                                                                            ; leg2  = { leg_sec_idx = OUT2; leg_mult = -2 }
                                                                                                                                                                                            ; leg3  = { leg_sec_idx = OUT3; leg_mult = 0 }
                                                                                                                                                                                          };;
                                                                                                                                                                                          
                                                                                                                                                                                          let books = {
                                                                                                                                                                                              book1 = { bid_info = Some { li_qty = 500; li_price = 50 } ; ask_info = Some { li_qty = 750 ; li_price = 50 }}
                                                                                                                                                                                            ; book2 = { bid_info = Some { li_qty = 200 ; li_price = 60 }; ask_info = Some { li_qty = 500 ; li_price = 70 }}
                                                                                                                                                                                            ; book3 = { bid_info = None ; ask_info = None }
                                                                                                                                                                                          };;
                                                                                                                                                                                          
                                                                                                                                                                                          let m = {
                                                                                                                                                                                            curr_time = 1
                                                                                                                                                                                          
                                                                                                                                                                                            ; last_ord_id = 0
                                                                                                                                                                                          
                                                                                                                                                                                            (* first strategy is 2*x1 - x2 + x3 *)
                                                                                                                                                                                            ; strat1 = (make_strat 1 2 (-1) 1)
                                                                                                                                                                                            (* second strategy is just the 3rd outright security *)
                                                                                                                                                                                            ; strat2 = (make_strat 2 0 1 0)
                                                                                                                                                                                          
                                                                                                                                                                                            (* outright books *)
                                                                                                                                                                                            ; out_book1 = {
                                                                                                                                                                                              b_buys = [ (make BUY 500 50 1 (Outright OUT1) 1 false 1) ]
                                                                                                                                                                                              ; b_sells = [ (make SELL 750 55 2 (Outright OUT1) 1 false 1) ]
                                                                                                                                                                                            }
                                                                                                                                                                                          
                                                                                                                                                                                            ; out_book2 = {
                                                                                                                                                                                              b_buys = [ (make BUY 200 60 3 (Outright OUT1) 1 false 1) ]
                                                                                                                                                                                              ; b_sells = [ (make SELL 500 70 4 (Outright OUT1) 1 false 1) ]
                                                                                                                                                                                            }
                                                                                                                                                                                          
                                                                                                                                                                                            ; out_book3 = {
                                                                                                                                                                                              b_buys = [ ]
                                                                                                                                                                                              ; b_sells = []
                                                                                                                                                                                            }
                                                                                                                                                                                          
                                                                                                                                                                                            (* Strategy books *)
                                                                                                                                                                                            ; s_book1 = {
                                                                                                                                                                                              b_buys = [
                                                                                                                                                                                              ]
                                                                                                                                                                                              ; b_sells = [
                                                                                                                                                                                                (make SELL 100 (-100) 5 (Strategy STRAT1) 1 false 1)
                                                                                                                                                                                              ]
                                                                                                                                                                                            }
                                                                                                                                                                                            ; s_book2 = empty_book
                                                                                                                                                                                          
                                                                                                                                                                                            (* Inbound and outbound message queues *)
                                                                                                                                                                                            ; inbound_msgs = []
                                                                                                                                                                                            ; outbound_msgs = []
                                                                                                                                                                                          } in
                                                                                                                                                                                          
                                                                                                                                                                                          let m' = implied_uncross_side BUY STRAT1 strat m in
                                                                                                                                                                                          
                                                                                                                                                                                          (*calc_implied_strat_order STRAT1 m.strat1 books BUY 1 *)
                                                                                                                                                                                          m'.outbound_msgs
                                                                                                                                                                                          
                                                                                                                                                                                          Out[24]:
                                                                                                                                                                                          val strat : strategy =
                                                                                                                                                                                            {time_created = 1; leg1 = {leg_sec_idx = OUT1; leg_mult = 1};
                                                                                                                                                                                             leg2 = {leg_sec_idx = OUT2; leg_mult = -2};
                                                                                                                                                                                             leg3 = {leg_sec_idx = OUT3; leg_mult = 0}}
                                                                                                                                                                                          val books : books_info =
                                                                                                                                                                                            {book1 =
                                                                                                                                                                                              {bid_info = Some {li_qty = 500; li_price = 50};
                                                                                                                                                                                               ask_info = Some {li_qty = 750; li_price = 50}};
                                                                                                                                                                                             book2 =
                                                                                                                                                                                              {bid_info = Some {li_qty = 200; li_price = 60};
                                                                                                                                                                                               ask_info = Some {li_qty = 500; li_price = 70}};
                                                                                                                                                                                             book3 = {bid_info = None; ask_info = None}}
                                                                                                                                                                                          - : outbound_msg list =
                                                                                                                                                                                          [Fill
                                                                                                                                                                                            {fill_client_id = 1; fill_qty = 100; fill_price = -95; fill_order_id = 5;
                                                                                                                                                                                             fill_order_done = true};
                                                                                                                                                                                           Fill
                                                                                                                                                                                            {fill_client_id = 1; fill_qty = 100; fill_price = 50; fill_order_id = 1;
                                                                                                                                                                                             fill_order_done = true};
                                                                                                                                                                                           Fill
                                                                                                                                                                                            {fill_client_id = 1; fill_qty = 200; fill_price = 70; fill_order_id = 4;
                                                                                                                                                                                             fill_order_done = true}]
                                                                                                                                                                                          

                                                                                                                                                                                          3.5 Implied uncrossing decomposition

                                                                                                                                                                                          In [25]:
                                                                                                                                                                                          (* Let's try to decompose the logic of 'implied_uncross_side' - we will put
                                                                                                                                                                                             several functions in the basis to focus on the critical aspects of the logic *)
                                                                                                                                                                                          #timeout 1000;;
                                                                                                                                                                                          
                                                                                                                                                                                          let d = Modular_decomp.top "implied_uncross_side"
                                                                                                                                                                                                  ~basis:["get_book_tops"; "allocate_implied_fills"; "insert_order";
                                                                                                                                                                                                  "create_fill_msgs"; "calc_implied_strat_order"] ~prune:true [@@program];;
                                                                                                                                                                                          
                                                                                                                                                                                          Out[25]:
                                                                                                                                                                                          val d : Top_result.modular_decomposition =
                                                                                                                                                                                            {Imandra_interactive.Modular_decomp.MD.md_session = 2i;
                                                                                                                                                                                             md_f =
                                                                                                                                                                                              {Imandra_surface.Uid.name = "implied_uncross_side"; id = <abstr>;
                                                                                                                                                                                               special_tag = <abstr>; namespace = <abstr>;
                                                                                                                                                                                               chash = Some FZmtlaFrhWJJV8XAu3gdJe1QzHeWahmEgShRYAM4YEY;
                                                                                                                                                                                               depth = (6i, 8i)};
                                                                                                                                                                                             md_args = [(sd : side);(s_id : strategy_id);(s : strategy);(m : market)];
                                                                                                                                                                                             md_regions = <abstr>}