SIX Swiss Exchange Pricing

Financial Services Exchange Infrastructure

Region decomposition analysis of SIX Swiss Exchange auction pricing logic — automatically enumerating all 44 distinct behavioral regions from seemingly simple conditional code.

Overview

This case study demonstrates region decomposition — one of ImandraX's most powerful analysis techniques — applied to a pricing component from SIX Swiss Exchange. Region decomposition automatically partitions the input space of an algorithm into distinct behavioral regions, each characterized by explicit constraints and invariant outputs.

What is Region Decomposition?

Region decomposition answers the question: "What are all the possible behaviors of this function?" It automatically enumerates every distinct execution path, producing a complete catalog of edge cases. See Region Decomposition for full documentation.

The Model

The complete pricing model is self-contained IML code you can paste into ImandraX.

Types

type order_type = Market | Limit | Quote
 
type order = {
  order_id : int;
  order_type : order_type;
  order_qty : int;
  order_price : real;
  order_time : int;
}
 
type fill_price =
  | Known of real
  | Unknown
 
type order_book = {
  buys : order list;
  sells : order list;
}

Helper Functions

let older_price o1 o2 =
  if o1.order_time > o2.order_time
  then o2.order_price else o1.order_price
 
let best_buy (ob : order_book) =
  match ob.buys with
  | x :: _ -> Some x
  | [] -> None
 
let best_sell (ob : order_book) =
  match ob.sells with
  | x :: _ -> Some x
  | [] -> None
 
let next_buy (ob : order_book) =
  match ob.buys with
  | [] -> None
  | [_] -> None
  | _ :: o2 :: _ -> Some o2
 
let next_sell (ob : order_book) =
  match ob.sells with
  | [] -> None
  | [_] -> None
  | _ :: o2 :: _ -> Some o2

Core Algorithm: `match_price`

The match_price function determines the fill price given an order book and a reference price. The branching logic follows specific rules for each order type combination:

let match_price (ob : order_book) (ref_price : real) =
  let bb = best_buy ob in
  let bs = best_sell ob in
  match bb, bs with
  | Some bb, Some bs ->
    begin
      match bb.order_type, bs.order_type with
      | (Limit, Limit) | (Quote, Quote) ->
        Known (older_price bb bs)
      | (Market, Market) ->
        if bb.order_qty <> bs.order_qty then Unknown
        else
          let bBid = match next_buy ob with
            | Some bestBuy ->
              if bestBuy.order_type = Market then None
              else Some bestBuy.order_price
            | _ -> None
          in
          let bAsk = match next_sell ob with
            | Some bestSell ->
              if bestSell.order_type = Market then None
              else Some bestSell.order_price
            | _ -> None
          in
          begin match bBid, bAsk with
          | (None, None) -> Known ref_price
          | (None, Some ask) ->
            if ask <. ref_price then Known ask
            else Known ref_price
          | (Some bid, None) ->
            if bid >. ref_price then Known bid
            else Known ref_price
          | (Some bid, Some ask) ->
            if bid >. ref_price then Known bid
            else if ask <. ref_price then Known ask
            else Known ref_price
          end
      | (Market, Limit) -> Known bs.order_price
      | (Limit, Market) -> Known bb.order_price
      | (Quote, Limit) ->
        if bb.order_time > bs.order_time then
          begin
            if bb.order_qty < bs.order_qty then Known bs.order_price
            else if bb.order_qty = bs.order_qty then
              match next_sell ob with
              | None -> Known bb.order_price
              | Some ord -> Known ord.order_price
            else Unknown
          end
        else Known bb.order_price
      | (Quote, Market) ->
        if bb.order_time > bs.order_time then
          begin
            if bb.order_qty < bs.order_qty then Known bs.order_price
            else if bb.order_qty = bs.order_qty then
              match next_sell ob with
              | None -> Known bb.order_price
              | Some ord -> Known ord.order_price
            else Unknown
          end
        else Known bb.order_price
      | (Limit, Quote) ->
        if bb.order_time > bs.order_time then
          begin
            if bs.order_qty < bb.order_qty then Known bb.order_price
            else if bb.order_qty = bs.order_qty then
              match next_buy ob with
              | None -> Known bs.order_price
              | Some ord -> Known ord.order_price
            else Unknown
          end
        else Known bs.order_price
      | (Market, Quote) ->
        if bb.order_time > bs.order_time then
          begin
            if bs.order_qty < bb.order_qty then Known bb.order_price
            else if bb.order_qty = bs.order_qty then
              match next_buy ob with
              | None -> Known bs.order_price
              | Some ord -> Known ord.order_price
            else Unknown
          end
        else Known bs.order_price
    end
  | _ -> Unknown

Region Decomposition

Decompose match_price to enumerate all distinct behaviors:

let d = match_price
[@@decomp top ~prune:true ()]

This produces 44 distinct regions, each characterized by explicit constraints on the order book structure and invariant fill price outputs.

Sample Regions

Region	Condition	Result
0	Empty sells list	`Unknown`
7	Market buyer + Limit seller	`Known(seller's price)`
8–22	Market/Market with equal quantities	Various rules examining secondary orders against reference price
23	Market/Market with quantity mismatch	`Unknown`

What the Decomposition Reveals

Regions 0–6 handle degenerate cases: empty order books, single-sided books, trivial matches
Region 7 is the canonical Market/Limit case — the seller's price is used directly
Regions 8–22 are all Market/Market with equal quantities, but differ in how secondary orders relate to the reference price. Each combination yields a different fill price formula.
Region 23 covers Market/Market with unequal quantities
Regions 24–44 cover Quote-involved combinations with timestamp-dependent priority

The fact that 15 of the 44 regions share the same top-level order type pairing (Market/Market, equal quantity) illustrates how deeply nested conditional logic can hide combinatorial complexity.

Test Instance Generation

Generate concrete test cases covering every region:

let d = match_price
[@@decomp top ~prune:true () |>> enumerate]

Each enumerated instance is a concrete test case satisfying a region's constraints, giving complete behavioral coverage with one test per region.

Exploring with Sample Orders

let order1 = {
  order_id = 1; order_type = Market;
  order_qty = 1000; order_price = 0.0; order_time = 123;
}
 
let order2 = {
  order_id = 2; order_type = Quote;
  order_qty = 250; order_price = 12.56; order_time = 125;
}
 
let order3 = {
  order_id = 3; order_type = Limit;
  order_qty = 250; order_price = 40.0; order_time = 125;
}
 
eval match_price { buys = [order1]; sells = [order3] } 10.0
(* Known 40.0 — Market buyer fills at Limit seller's price *)
 
eval match_price { buys = [order2]; sells = [order3] } 10.0
(* Known 40.0 — Quote buyer fills at older order's price *)

Results

Complexity Hidden in Simplicity

What looks like a straightforward price matching algorithm actually has 44 distinct behavioral modes. Without region decomposition, ensuring correct behavior across all modes would require manually reasoning about every combination — a task that scales combinatorially with code complexity.

Region decomposition provides:

Complete behavioral catalog — every possible execution path is explicitly characterized
Edge case discovery — surprising interactions between order types are surfaced automatically
Regression testing — the region catalog serves as a specification for future changes
Regulatory documentation — each region can be mapped to specific regulatory requirements

44 Behavioral Regions

Automatically discovered from seemingly simple pricing logic — each with explicit constraints.

Complete Analysis

Every possible execution path enumerated — no edge case left undiscovered.

Production Deployed

Region decomposition is used in production at leading financial institutions for ongoing verification.