Tata Institute of Fundamental Research, Mumbai, India<EMAIL_ADDRESS>Tata
Institute of Fundamental Research, Mumbai, India<EMAIL_ADDRESS>Birla Institute of Technology and Science Pilani, Goa, India.
<EMAIL_ADDRESS>Raja Natarajan, Suneel Sarswat, and Abhishek Kr. Singh
[500]Information systems Online auctions [500]Software and its engineering
Formal software verification [300]Theory of computation Algorithmic mechanism
design [300]Theory of computation Computational pricing and auctions
[100]Theory of computation Program verification [100]Theory of computation
Automated reasoning

# Verified Double Sided Auctions for Financial Markets

Raja Natarajan  Suneel Sarswat  Abhishek Kr Singh

###### Abstract

Double sided auctions are widely used in financial markets to match demand and
supply. Prior works on double sided auctions have focused primarily on single
quantity trade requests. We extend various notions of double sided auctions to
incorporate multiple quantity trade requests and provide fully formalized
matching algorithms for double sided auctions with their correctness proofs.
We establish new uniqueness theorems that enable automatic detection of
violations in an exchange program by comparing its output with that of a
verified program. All proofs are formalized in the Coq proof assistant without
adding any axiom to the system. We extract verified OCaml and Haskell programs
that can be used by the exchanges and the regulators of the financial markets.
We demonstrate the practical applicability of our work by running the verified
program on real market data from an exchange to automatically check for
violations in the exchange algorithm.

###### keywords:

Double Sided Auction, Formal Verification, Financial Markets, Proof Assistant

##  1 Introduction

Computer algorithms are routinely deployed nowadays by all big stock exchanges
to match buy and sell requests. These algorithms are required to abide by
various regulatory guidelines. For example, market regulators make it
mandatory for trades resulting from double sided auctions at exchanges to be
fair, uniform and individual-rational.

In this paper, we introduce a formal framework for analyzing trades resulting
from double sided auctions used in the financial markets. To verify the
essential properties required by market regulators, we formally define these
notions in a theorem prover and then develop important results about matching
demand and supply. Finally, we use this framework to verify properties of two
important classes of double sided auction mechanisms.

One of the resulting advantages of our work for an exchange or a regulator is
that they can check the algorithms deployed for any violations from required
properties automatically. This is enabled by the new uniqueness results that
we establish in this work. All the definitions and results presented in this
paper are completely formalized in the Coq proof assistant without adding any
additional axioms to it. The complete formalization in Coq facilitates
automatic program extraction in OCaml and Haskell, with the guarantee that
extracted programs satisfy the requirements specified by the market regulator.
Consequently, the extracted program could also be deployed directly at an
exchange, apart from checking for violations in existing programs. We
demonstrate the practical applicability of our work by running the verified
program on real market data from an exchange to automatically check for
violations in the exchange algorithm.

The rest of this paper is organized as follows: Section 2 provides a brief
background and overview of trading at exchanges which is needed to describe
our contributions; In Section 3, we briefly state our contributions; Section 4
provides basic definitions and establishes certain combinatorial results;
Section 5 describes a fairness procedure; Section 6 describes the uniform
matching mechanism used in the financial markets; Section 7 describes the
maximum matching mechanism; Section 8 establishes uniqueness results that
enables automatic checking for violations in an exchange matching algorithm;
Section 9 describes the practical utility of our work through running our
verified program on real market data from an exchange; Section 10 concludes
the paper with related work and future directions. Parts of some sections have
been moved to the appendix.

##  2 Background

Financial trades occur at various types of exchanges. For example, there are
exchanges for stocks, commodities and currencies. At any exchange, multiple
buyers and sellers participate to trade certain products. Mostly exchanges
employ double sided auction mechanisms to match the buyers and sellers. Some
exchanges, apart from using double sided auctions, also use an online
continuous algorithm for executing trades during certain time intervals,
especially for highly traded products.

For conducting trades of a certain product using a double sided auction
mechanism, the exchange collects buy and sell requests from the traders for a
fixed time period. At the end of this time period, the exchange matches some
of the trade requests and outputs trades, all at a single price. This price is
sometimes referred to as the equilibrium price and the process as price
discovery. A buyer places a buy request, also known as a _bid_ , which
consists of a quantity indicating the maximum number of units he is interested
in buying and a common maximum price (bid’s limit price) for each of the
units. Similarly, a seller’s sell request, an _ask_ , consists of a quantity
and a minimum price (ask’s limit price). Each trade (_transaction_) consists
of a bid, an ask, traded quantity, and a trade price. Naturally, the traded
quantity should be at most the minimum of the bid and the ask quantities and
the trade price should be compatible with the bid and the ask.

Apart from the single price property and compatibility constraint mentioned
above, there are other desired properties that the trades (_matching_) should
have. The properties that capture these constraints are: _uniform_ ,
_individual-rational_ , _fair_ and _maximum_. We briefly describe these
matching properties:

  * •

Uniform: A matching is uniform if all the trades happen at the same price.

  * •

Individual-rational: A matching is individual-rational if for each matched
bid-ask pair the trade price is between the bid and ask limit prices. In the
context of financial markets, the trade price should always be between the
limit prices of the matched bid-ask pair.

  * •

Fair: A bid $b_{1}$ is more competitive than a bid $b_{2}$ if $b_{1}$ has a
higher limit price than $b_{2}$ or if their limit prices are the same and
$b_{1}$ arrives earlier than $b_{2}$. Similarly, we can define competitiveness
between two asks. A matching is _unfair_ if a less competitive bid gets
matched but a more competitive bid is not fully matched. Similarly, it could
be unfair if a more competitive ask is not fully matched. If a matching is not
unfair, then it is fair.

  * •

Maximum: A matching is maximum if it has the maximum possible total traded
quantity among all possible matchings.

  * •

Optimal individual-rational-uniform: An individual-rational and uniform
matching is called optimal individual-rational-uniform if it has the largest
total trade volume among all matchings that are individual-rational and
uniform.

No single algorithm can possess all the above first four properties
simultaneously [11, 5]. In the context of financial markets, regulators insist
on the matching being fair and optimal individual-rational-uniform, thus
compromising on the maximum property. In other contexts where the matching
being maximum is important along with individual rational and fair, uniformity
is lost. This gives rise to two different classes of double sided auction
mechanisms, each with a different objective. In our work, we consider both
these classes of mechanisms.

##  3 Our Contributions

In this work, we formalize the notion of double sided auctions where trade
requests can be of multiple quantities. Prior to our work, similar notions
were explicitly defined only for single unit trade requests [8, 6, 12]. In
going from formalizing the theory for single unit to the theory of multiple
units, the mechanisms and their correctness proofs changed substantially. Due
to the possibility of partial trades, the formal analysis of multiple unit
trades becomes significantly more involved than in [8]. In this work, we show
how to efficiently handle this extra complexity by making the functions and
their properties sensitive to the partial trade quantities. This helps us to
develop formal proofs of correctness of the recursive mechanisms for double
sided auctions.

In addition, we provide new uniqueness results that guarantee that the
matching algorithm for the double sided auctions used in the financial markets
outputs a unique volume of trades per order if the algorithm is fair and
optimal individual-rational-uniform; thus enabling automatic checking of
violations in the exchange algorithm by comparing its output with that of a
verified program. We demonstrate this by running the extracted OCaml code of
our certified mechanism on real data from an exchange and comparing the
outputs. Following is a brief description of the key results formalized in
this work.

  * •

Combinatorial result: We show that the modeling and the libraries we created
to obtain our results are also useful in proving other important results on
double sided auctions. For example, in Theorem 4.7, we show that for any $p$,
no matching can achieve a trade volume higher than the sum of the total demand
and the total supply in the market at price $p$.

  * •

Fairness: We show that any matching can be converted into a fair matching
without compromising on the total traded volume. For this, we design an
algorithm, the $\mathsf{Fair}$ procedure, which takes a matching $M$ as input,
and outputs a matching $M^{\prime}$. In Theorem 5.7, we show that the total
traded quantities of $M$ and $M^{\prime}$ are the same and $M^{\prime}$ is a
fair matching.

  * •

Uniform mechanism: We design an algorithm, the $\mathsf{UM}$ procedure, that
takes as input the bids and the asks and outputs a fair, individual-rational
and uniform matching. Furthermore, in Theorem 6.5, we show that the output
matching has the largest total trade volume among all the matchings that are
uniform and individual-rational and thus is optimal individual-rational-
uniform. This algorithm is used in the exchanges that output trades using
double sided auctions.

  * •

Maximum mechanism: We design an algorithm, the $\mathsf{MM}$ procedure, that
takes as input the bids and the asks and outputs an individual-rational, fair
and maximum matching. In Theorem 7.1, we show that the output matching has the
largest total trade volume among all the matchings that are individual-
rational.

  * •

Uniqueness theorems: For any two fair and optimal individual-rational-uniform
matchings, Theorem 8.2 implies that their total trade volume for each order is
the same. Thus, if we compare the trade volumes between an exchange’s matching
output with our verified program’s output and for some order they do not
match, then the exchange’s matching is not fair and optimal individual-
rational-uniform. On the contrary, if for each order, the trade volumes match,
then Theorem 8.3 implies that the exchange’s matching is also fair and optimal
individual-rational-uniform (given that it already is individual-rational and
uniform, which can be easily verified by checking the trade prices). Making
use of these results, in Section 9, we check violations automatically in real
data from an exchange.

The Coq code together with the extracted OCaml and Haskell programs for all
the above results is available at [1]. Our Coq formalization consists of
approximately 50 new definitions, 750 lemmas and theorems and 12000 lines of
code. In the following sections, we provide definitions, procedures and proof
sketches that closely follow our actual formalization.

##  4 Modeling Double Sided Auctions

In a double sided auction multiple buyers and sellers place their orders to
buy or sell an underlying product. The auctioneer matches these buy-sell
requests based on their _limit prices_ , _arrival time_ , and the maximum
specified _trade quantities_. Note that the limit prices are natural numbers
when expressed in the monetary unit of the lowest denomination (like cents in
USA). In our presentation, we will be working with lists (of bids, asks and
transactions); For ease of readability, we will often use set-theoretic
notations like $\in$, $\subseteq$, $\supseteq$, $\emptyset$ on lists whose
meanings are easy to guess from the context.

######  Definition 4.1.

Bid: A bid $b=(id_{b},\tau_{b},q_{b},p_{b})$ represents a buy request having
four components. Here, the first two components $id_{b}$ and $\tau_{b}$ are
the unique identifier and the timestamp assigned to the buy request $b$,
respectively, whereas the third component $q_{b}$ represents the quota of $b$,
the maximum quantity of the item the buyer is willing to buy. The last
component $p_{b}$ is the limit price of the buy request, which is the price
above which the buyer does not want to buy the item.

######  Definition 4.2.

Ask: An ask $a=(id_{a},\tau_{a},q_{a},p_{a})$ represents a sell request having
four components. Here, the first two components $id_{a}$ and $\tau_{a}$ are
the unique identifier and the timestamp assigned to the sell request $a$,
respectively, whereas the third component $q_{a}$ represents the quota of $a$,
the maximum quantity of the item the seller is willing to sell. The last
component $p_{a}$ is the limit price of the sell request, which is the price
below which the seller does not want to sell the item.

We say that a bid $b\in B$ is matchable with an ask $a\in A$ if $p_{a}\leq
p_{b}$.

In a double sided auction, the auctioneer is presented with duplicate-free111A
list of bids or asks is duplicate-free if all the participating orders have
distinct ids. lists of buy and sell requests (lists $B$ and $A$,
respectively). The auctioneer can match a bid $b\in B$ with an ask $a\in A$
only if $p_{b}\geq p_{a}$. Furthermore, the auctioneer assigns a trade price
and a trade quantity to each matched bid-ask pair, which finally results in a
_transaction_ $m$. Therefore, we can represent a matching of demand and supply
by using a list whose entries are _transactions_.

######  Definition 4.3.

Transaction: A transaction $m=(b_{m},a_{m},q_{m},p_{m})$ describes a trade
between the bid $b_{m}$ and the ask $a_{m}$. The next two components $q_{m}$
and $p_{m}$ are the traded quantity and the trade price, respectively. For
ease of readability, we use the terms $p(b_{m})$, $p(a_{m})$, $q(b_{m})$, and
$q(a_{m})$ for $p_{b_{m}}$, $p_{a_{m}}$, $q_{b_{m}}$ and $q_{a_{m}}$,
respectively.

######  Definition 4.4.

(Matching M B A): A list of transactions $M$ is a matching between the
duplicate-free lists of bids $B$ and asks $A$ if

  1. 1.

For each transaction $m\in M$, the bid of $m$ is matchable with the ask of $m$
(i.e., $p(a_{m})\leq p(b_{m})$).

  2. 2.

The list of bids present in $M$, denoted by $B_{M}$, is a subset of $B$ (i.e.,
$B_{M}\subseteq B$).

  3. 3.

The list of asks present in $M$, denoted by $A_{M}$, is a subset of $A$ (i.e.,
$A_{M}\subseteq A$).

  4. 4.

For each bid $b\in B$, the total traded volume of bid $b$ in the matching $M$,
denoted by $Q(b,M)$, is not more than its maximum quantity (i.e., $\text{ for
all }b\in B,Q(b,M)\leq q_{b}$).

  5. 5.

For each ask $a\in A$, the total traded volume of ask $a$ in the matching $M$,
denoted by $Q(a,M)$, is not more than its maximum quantity (i.e. $\text{ for
all }a\in A,Q(a,M)\leq q_{a}$).

_Description_. Note that there might be some bids in $B$ which are not matched
to any asks in $M$ and some asks in $A$ which are not matched to any bids in
$M$.

######  Note 4.5.

For simplicity, with slight abuse of notation, we use $Q$ to denote total
quantity of various objects which will be clear from the context. So, $Q(b,M)$
and $Q(a,M)$ represent the total quantities of the bid $b$ and the ask $a$
traded in the matching $M$, respectively. Similarly, the terms $Q(B)$ and
$Q(A)$ denote the sum of the quantities of all the bids in $B$ and the sum of
the quantities of all the asks in $A$, respectively. And also, for the total
traded quantity in a matching $M$, we use the term $Q(M)$. However, in the Coq
implementation, each of these terms are represented by different names:
$\mathsf{QMb},\mathsf{QMa},\mathsf{QB},\mathsf{QA}\text{ and }\mathsf{QM}$.

Formalization notes: We have defined Bid, Ask and Transaction as record types
in Coq. We define the proposition _matching_in B A M_ to be true if and only
if $M$ is a matching between the list of bids $B$ and the list of asks $A$.

###  4.1 Matching Demand and Supply

Let $B_{\geq p}$ represents the list of bids in $B$ whose limit prices are at
least a given number $p$. Similarly, $A_{\leq p}$ represents the list of asks
in $A$ whose limit prices are at most $p$. Therefore, the quantities
$Q(B_{\geq p})$ and $Q(A_{\leq p})$ represents the total demand and the total
supply of the product at the price $p$ in the market, respectively. Although,
in general we cannot say much about the relationship between the total demand
(i.e. $Q(B_{\geq p})$) and supply (i.e. $Q(A_{\leq p})$) at an arbitrary price
$p$, we can prove the following important results about the traded quantities
of the matched bid-ask pairs.

######  Lemma 4.6.

If $M$ is a matching between the list of bids $B$ and the list of asks $A$,
then

$\displaystyle Q(M)=\sum_{b\in B}Q(b,M)\leq\sum_{b\in B}q_{b}=Q(B)\text{ and
}Q(M)=\sum_{a\in A}Q(a,M)\leq\sum_{a\in A}q_{a}=Q(A)$

######  Theorem 4.7.

If $M$ is a matching between the list of bids $B$ and the list of asks $A$,
then for all natural numbers $p$, we have $Q(M)\leq Q(B_{\geq p})+Q(A_{\leq
p})$

Theorem 4.7 states that no matching $M$ can achieve a trade volume higher than
the sum of the total demand and supply in the market at any given price.

_Proof Idea._ We first partition the matching $M$ into two lists:
$M_{1}=\\{m\in M\mid p(b_{m})\geq p\\}$ and $M_{2}=\\{m\in M\mid
p(b_{m})<p\\}$. Thus, $Q(M)=Q(M_{1})+Q(M_{2})$.

It is easy to see that $M_{1}$ is a matching between $B_{\geq p}$ and $A$, and
hence from Lemma 4.6, $Q(M_{1})\leq Q(B_{\geq p})$.

Next, we prove that $M_{2}$ is a matching between $B$ and $A_{\leq p}$.
Consider a transaction $m$ from $M_{2}$. Since $m\in M$, $p(b_{m})\geq
p(a_{m})$, and from the definition of $M_{2}$, we have $p(b_{m})<p$. This
implies $p(a_{m})<p$, i.e., asks of $M_{2}$ come from $A_{\leq p}$. Hence,
$M_{2}$ is a matching between $B$ and $A_{\leq p}$, and applying Lemma 4.6, we
have $Q(M_{2})\leq Q(A_{\leq p})$.

Combining, we have $Q(M)=Q(M_{1})+Q(M_{2})\leq Q(B_{\geq p})+Q(A_{\leq p})$,
which completes the proof of Theorem 4.7. $\square$

Formalization notes: The formal proof of Theorem 4.7 is completed by first
proving the Lemmas _Mbgep_bound_ ($Q(M_{1})\leq Q(B_{\geq p})$) and
_Mbltp_bound_ ($Q(M_{2})\leq Q(A_{\leq p})$) and then combining them in
theorem _bound_on_M_. These results can be found in the file ’Bound.v’.

###  4.2 Individual-Rational Trades

An auctioneer assigns a trade price to each matched bid-ask pair. In any
matching it is desired that the trade price of a bid-ask pair lies between
their limit prices. A matching which has this property is called an
_individual-rational (IR)_ matching.

######  Definition 4.8.

$\mathsf{Is\\_IR}(M):=\text{ for all }m\in M,\ p(b_{m})\geq p_{m}\geq
p(a_{m})$.

Note that any matching can be converted to individual-rational by changing the
price of each transaction to lie between the limit prices of its bid and ask
(See Fig 1).

$]$$]$6969$]$$]$8282$]$$]$9191$]$$]$112112$]$$]$125125$[$$[$5252$[$$[$7979$[$$[$8585$[$$[$9898$[$$[$113113$M_{2}$$M_{1}$

Figure 1:  The colored dots represent trade prices for matched bid-ask pairs.
Matching $M_{2}$ is not IR but $M_{1}$ is IR, even though both the matchings
contain exactly the same bid-ask pairs.

##  5 Fairness in Competitive Markets

A double sided auction is a competitive event, where the priority among
participating traders is determined by various attributes of the orders. A bid
with higher limit price is considered more _competitive_ compared to bids with
lower limit prices. Similarly, an ask with lower limit price is considered
more competitive compared to asks with higher limit prices. Ties are broken in
favor of the requests that have an earlier arrival time. A matching which
prioritizes more competitive traders is called a _fair_ matching.

######  Definition 5.1 (Arrow notation).

$\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}L$ denotes that the list $L$
is sorted as per the competitiveness of the bids in $L$, with the most
competitive bid being on top. Similarly,
$\stackrel{{\scriptstyle\mathbb{A}}}{{\uparrow}}L$ denotes that the list $L$
is sorted as per the competitiveness of the asks in $L$, with the most
competitive ask being on top. Similarly we can define
$\stackrel{{\scriptstyle\mathbb{A}}}{{\downarrow}}$ and
$\stackrel{{\scriptstyle\mathbb{B}}}{{\downarrow}}$ for sorting lists where
the most competitive orders lie at the bottom.

In this section, we show that there exists a procedure $\mathsf{Fair}$ that
takes a matching $M$ between bids $B$ and asks $A$ as input and outputs a fair
matching $M^{\prime}=\mathsf{Fair}(M,B,A)$ with the same trade volume as that
of $M$. To describe the $\mathsf{Fair}$ procedure, we will need the following
definitions.

######  Definition 5.2.

Let $M$ be a matching between bids $B$ and asks $A$.

  * •

$M$ is fair on bids if for all pairs of bids $b_{1},b_{2}\in B$ such that
$b_{1}$ is more competitive than $b_{2}$ and $b_{2}$ participates in the
matching $M$, then $b_{1}$ is fully traded in $M$ (i.e.,
$Q(b_{1},M)=q(b_{1})$).

  * •

Similarly, $M$ is fair on asks if for all pairs of asks $a_{1},a_{2}\in A$
such that $a_{1}$ is more competitive than $a_{2}$ and $a_{2}$ participates in
the matching $M$, then $a_{1}$ is fully traded in $M$ (i.e.,
$Q(a_{1},M)=q(a_{1})$).

  * •

$M$ is fair if it is both fair on bids and asks.

The $\mathsf{Fair}$ procedure works in two steps: first, it sorts the matching
$M$ and the asks $A$ based on the competitiveness of the asks and then runs on
them a procedure "fair on asks" $\mathsf{FOA}$ that outputs a matching
$M^{\prime}$ that is of the same volume as that of $M$ and is fair on the
asks. In the second step, it sorts the resulting matching $M^{\prime}$ and the
bids $B$ based on the competitiveness of the bids and then runs on them a
procedure fair on bids $\mathsf{FOB}$ that outputs a matching
$M^{\prime\prime}$ that is of the same volume as that of $M^{\prime}$ and is
fair on the bids. The $\mathsf{Fair}$ procedure returns $M^{\prime\prime}$ as
its output. The procedures $\mathsf{FOB}$ and $\mathsf{FOA}$, along with their
correctness proofs, mirror each other and we just describe $\mathsf{FOB}$
below and show that
$\mathsf{FOB}(\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}M^{\prime},\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}B)$
outputs a fair on bids matching and has the same trade volume as that of
$M^{\prime}$. Furthermore, we will show that if $M^{\prime}$ is fair on asks,
then
$\mathsf{FOB}(\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}M^{\prime},\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}B)$
is fair on asks. This will immediately imply that the procedure
$\mathsf{Fair}(M,B,A)$ outputs a fair matching with the same total trade
volume as that of $M$.

###  5.1 Fair on Bids

To describe the fair on bids $\mathsf{FOB}$ procedure, we first need the
following notation.

######  Definition 5.3.

Given a list $L$ and and an element $a$, $a::L$ denotes the list whose top
element (head) is $a$ and the following elements (tail) are the elements of
$L$ (in the same order as they appear in $L$).

The $\mathsf{FOB}$ procedure takes sorted (based on the bids’ competitiveness)
lists of transactions $M$ and bids $B$. Intuitively, when all the bids are of
unit quantity, we want to scan the list of transactions in $M$ from top to
bottom replacing the bids therein with the bids of $B$ from top to bottom. So,
in effect, in the $\mathsf{FOB}$ procedure we will implement this intuition
apart from taking care of multiple quantity bids; and also make the procedure
recursive so that we can provide a formalization friendly inductive proof of
correctness. Let $B=b::B^{\prime}$ and $M=m::M^{\prime}$. In our procedure, we
first pick the top bid $b$ of $B$ and the top transaction $m$ of $M$, and
compare $q_{b}$ with $q_{m}$. Now we have three cases. In each of the three
cases, the procedure first outputs a transaction between the bid $b$ and the
ask of $m$ of quantity $\min\\{q_{m},q_{b}\\}$. Case I: If $q_{b}=q_{m}$, we
remove $b$ and $m$ from their respective lists and recursively solve the
problem on $B^{\prime}$ and $M^{\prime}$. Case II: If $q_{b}<q_{m}$, we remove
$b$ from the list $B$ and update $q_{m}$ to $q_{m}-q_{b}$ and recursively
solve the problem on $B^{\prime}$ and $M$. Case III: If $q_{b}>q_{m}$, we
remove $m$ from the list $M$ and set a parameter $t$ to $q_{m}$ that we will
send to the recursive call along with $M^{\prime}$ and $B$. The parameter $t$
informs our recursive procedure that the top element $b$ of $B$ has
effectively quantity $q_{b}-t$. Thus, our procedure will take three
parameters: the list of transactions, the list of bids and the parameter $t$
(Note that unlike Case II ($q_{b}<q_{m}$) where the top transaction is
updated, the top bid is not updated in Case III ($q_{b}>q_{m}$). This is done
for technical reasons: Later we need to prove that the set of bids of
$\mathsf{FOB}$ is a subset of $B$, and at the same time we have to ensure that
the total traded quantity of the bid $b$ in the matching outputted by
$\mathsf{FOB}$ remains below its maximum quantity $q_{b}$, as required by the
matching property. This would not be possible to do if we updated $B$ and
hence we take this approach of keeping the total traded quantity of the top
bid $b$ in a separate argument: $t$ of $f$.). Keeping this description in
mind, we now formally define the procedure $\mathsf{FOB}$.

######  Definition 5.4.

Fair On Bid ($\mathsf{FOB}$).

$\displaystyle\mathsf{FOB}(M,B)=f(M,B,0)$ $\displaystyle\text{where
}f(M,B,t)=$ $\displaystyle\begin{cases}nil&\text{ if $M=nil$ or $B=nil$}\\\
(b,a_{m},q_{m},p_{m})::f(M^{\prime},B^{\prime},0)&\text{if $q_{m}=q_{b}-t$}\\\
(b,a_{m},q_{m},p_{m})::f(M^{\prime},b::B^{\prime},t+q_{m})&\text{if
$q_{m}<q_{b}-t$}\\\
(b,a_{m},q_{b}-t,p_{m})::f((b_{m},a_{m},q_{m}-(q_{b}-t),p_{m})::M^{\prime},B^{\prime},0)&\text{if
$q_{m}>q_{b}-t$}\end{cases}$

where $M=m::M^{\prime}$ when $M\neq nil$ and $B=b::B^{\prime}$ when $B\neq
nil$.

_Description_. In non-trivial cases (i.e. $M\neq nil$ and $B\neq nil$) the
function call $\mathsf{FOB}(M,B)$ reduces to $f(M,B,0)$.

######  Theorem 5.5.

Let $M$ be a matching between bids $B$ and asks $A$ where the lists $M$ and
$B$ are sorted in the descending order of the competitiveness of their bids
(i.e., the most competitive bid and the transaction with the most competitive
bid are on top of their respective lists). Let $M_{\beta}=\mathsf{FOB}(M,B)$,
then

  1. (a)

$M_{\beta}$ is a matching between bids $B$ and asks $A$.

  2. (b)

For each ask $a\in A$, the total traded quantity of $a$ in $M$ is same as the
total traded quantity of $a$ in $M_{\beta}$ (i.e., $Q(a,M)=Q(a,M_{\beta})$).
As a corollary, we get that if $M$ is fair on asks, then $M_{\beta}$ is also
fair on asks.

  3. (c)

The total traded quantity of $M$ is equal to the total traded quantity of
$M_{\beta}$ (i.e., $Q(M)=Q(M_{\beta})$).

  4. (d)

The matching $M_{\beta}$ is fair on bids.

_Proof Outline_. Here, we briefly describe certain aspects of the proof; more
details can be found in Appendix B and for the complete formalization see [1].
Note that in each of the recursive calls in $f$, either the size of the first
argument $|M|$ decreases or the size of the second argument $|B|$ decreases.
Therefore, we prove the above statements using (well founded) induction on the
sum $(|M|+|B|)$. Proof of (a) and (b) is done using induction and case
analysis. The proof of (c) follows by combining Lemma 4.6 with (b). We focus
on the proof of (d) below.

Let bid $b$ be the top element of the bids $B$ and $B=b::B^{\prime}$. First,
we prove two general results:

$\text{For all }t,\text{ if }Q(M)\geq q_{b}-t,\text{ then
}Q(f(M,b::B^{\prime},t),b)=q_{b}-t,$

which states that if the total trade volume of the matching $M$ is at least
$q_{b}-t$, then in the matching $f(M,b::B^{\prime},t)$ the top bid $b$ has
trade quantity $q_{b}-t$. The proof of this can be done using induction on the
size of $M$. Intuitively, $f$ tries to match as much quantity of the top bid
$b$ with the top transaction in $M$. When the call $f(M,b::B^{\prime},t)$ is
made, the top bid $b$ already has $t$ traded quantity and $q_{b}-t$ of its
quantity remains untraded. If the quantity of the top transaction $m$ of $M$
is at least $q_{b}-t$, then we are done. Otherwise, $f$ matches $q_{m}$
quantities of $b$ and recursively calls $f$ on a smaller list and then we will
be done by applying the induction hypothesis.

Now, we state the second general result.

$\text{For all }t,\text{ if distinct bids }b,b^{\prime}\text{ belong to the
bids of }f(M,b::B^{\prime},t),\text{ then }Q(M)\geq q_{b}-t.$

This result can be proved, like the previous result, using induction on the
sum ($|M|+|B|$); see [1] for details. Intuitively, since $b^{\prime}$ is
matched by $f(M,b::B^{\prime},t)$ (in particular $b^{\prime}\in B^{\prime}$),
then $f(M,b::B^{\prime},t)$ will completely match $b$ (which has at least
$q_{b}-t$ quantity remaining untraded) before it matches even a single
quantity of $b^{\prime}$.

Now using the above general results, we prove (d). We need to show the
following: for all $b_{1},b_{2}\in B$, if $b_{1}$ is more competitive than
$b_{2}$ and $Q(\mathsf{FOB}(M,B),b_{2})\geq 1$, then
$Q(\mathsf{FOB}(M,B),b_{1})=q_{b_{1}}$, i.e., if the bid $b_{2}$ participates
in the matching $M$ then the bid $b_{1}$ is fully traded in $M$. Fix
$b_{1},b_{2}\in B$ such that $b_{1}$ is more competitive than $b_{2}$ and
$Q(\mathsf{FOB}(M,B),b_{2})\geq 1$. Note that the bid $b_{2}$ cannot be equal
to the bid $b$ since bids $B$ are sorted. Now we analyze three possible cases:
$b_{1}\neq b$, $b_{1}=b$ and $Q(M)\geq q_{b}$, and $b_{1}=b$ and $Q(M)<q_{b}$.

  * •

In the case when $b_{1}\neq b$, we consider the recursive call where $b_{1}$
is the top bid in the argument for the first time. In this recursive call the
list of bids is smaller than $B$ since the bid $b$ must be fully traded
before. Then, we are immediately done by applying the induction hypothesis.

  * •

In the case $b_{1}=b$ and $Q(M)\geq q_{b}$, in the matching
$\mathsf{FOB}(M,b::B^{\prime})=f(M,b::B^{\prime},0)$ the top bid $b$ has total
trade volume $q_{b}-0=q_{b}$ from the first general result invoked with $t=0$,
and hence $b_{1}=b$ is fully traded.

  * •

In the case $b_{1}=b$ and $Q(M)<q_{b}$, we arrive at the contradiction
$Q(M)\geq q_{b}$ by invoking the second general result with $t=0$, $b=b_{1}$,
$b^{\prime}=b_{2}$ and $\mathsf{FOB}(M,b::B^{\prime})=f(M,b::B^{\prime},0)$.

$\square$

Similar to the procedure $\mathsf{FOB}$, we have a procedure $\mathsf{FOA}$,
that produces a fair matching on asks (see [1]). Combining the $\mathsf{FOA}$
and $\mathsf{FOB}$ procedures, we have the following definition of the
$\mathsf{Fair}$ procedure.

######  Definition 5.6.

$\mathsf{Fair}(M,B,A)=\mathsf{FOB}(\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}\mathsf{FOA}(\stackrel{{\scriptstyle\mathbb{A}}}{{\uparrow}}M,\stackrel{{\scriptstyle\mathbb{A}}}{{\uparrow}}A),\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}B)$.

We conclude this section by formally summarizing the main fairness result.

######  Theorem 5.7.

If $M$ is a matching on the list of bids $B$ and the list of asks $A$, then
the matching $M^{\prime}=\mathsf{Fair}(M,B,A)$ on $B$ and $A$ is a fair
matching such that $Q(M)=Q(M^{\prime})$.

Formalization notes: The procedure $\mathsf{FOB}$ and $\mathsf{FOA}$ are
implemented in Coq using the Equations plugin which is helpful to write
functions involving well-founded recursion [9]. The proof of Theorem 5.7 is
quite extensive and done in several parts. First we prove all the parts of
Theorem 5.5 in the file ’mFair_Bid.v’. We prove similar theorems for the
procedure $\mathsf{FOA}$ in ’mFair_Ask.v’ file. Later all the results are
combined in the file ’MQFair.v’ and the above theorem is proved as
_exists_fair_matching_.

##  6 Uniform Price Matchings in Financial Markets

Liquidity in a market is a measure of how quickly one can trade in that market
and maximizing the total trade volume helps increase liquidity. However, to
maximize the total trade volume sometimes we have to accept different trade
prices to the matched bid-ask pairs (Fig 2).

$85$$100$$90$$70$$85$$100$$90$$70$$B$$A$$B$$A$(a) $UM$(b) $MM$

Figure 2: Both the bids and the asks have quantity one. The only individually
rational matching of size two is not uniform.

Assigning different trade prices for the same product in the same market
simultaneously, might lead to dissatisfaction among some traders. As stated in
the introduction, in the financial markets, the matching should be fair and
optimal individual-rational-uniform. In this section, we describe the
$\mathsf{UM}$ process that takes as input a list of bids and a list of asks
and produces a fair and optimal individual-rational-uniform matching that can
be directly applied in the financial markets for conducting double sided
auctions. We present a novel proof of optimality of the $\mathsf{UM}$ process.

Before we describe the $\mathsf{UM}$ process, we first give some intuition.
Observe that in any individual-rational and uniform matching $M$ all the
buyers are matched at a single price $p$ and the price $p$ lies between the
limit prices of all the matched bid-ask pairs. This means all the matched
bids’ limit prices are at least $p$ and all the matched asks’ limit prices are
at most $p$. In the special case when all the orders are of unit quantity, the
matching can be visualized as a fully nested balanced parenthesis (for
example, [[[[ ]]]]) where each bid is represented by a closed parenthesis ‘]’
and each ask as an open parenthesis ‘[’ (See Figure 1).

Now, we describe the $\mathsf{UM}$ process. We recursively pair the most
competitive available bid with the most competitive available ask, if they are
matchable. The trade quantity for each matched bid-ask pair is the minimum of
the remaining quantities of the respective bid and the ask. The trade price
assigned to each pair is the price of the ask in that pair222Observe that any
value in the interval of the limit prices of the matched bid-ask pair can be
assigned as the trade price and it will not affect any analysis done in this
work.. We terminate the process once there are no more matchable bid-ask pairs
remaining. At the end of the process, to produce a uniform matching we have to
assign a single trade price to all the matched bid-ask pairs which we choose
to be the trade price of the last matched bid-ask pair (which also keeps the
individual-rational property intact).

Keeping this description in mind, we now formally define the $\mathsf{UM}$
process using recursion.

######  Definition 6.1.

Uniform Matching ($\mathsf{UM}$).

$\displaystyle\mathsf{UM}(B,A)=\mathsf{Replace\\_prices}(f_{u}(\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}B,\stackrel{{\scriptstyle\mathbb{A}}}{{\uparrow}}A,0,0),\mathsf{Last\\_trade\\_price}(f_{u}(\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}B,\stackrel{{\scriptstyle\mathbb{A}}}{{\uparrow}}A,0,0)))$
$\displaystyle\text{where }f_{u}(B,A,t_{b},t_{a})=$
$\displaystyle\begin{cases}nil&\text{if $B=nil$ or $A=nil$ or
$p_{b}<p_{a}$}\\\
(b,a,q_{b}-t_{b},p_{a})::f_{u}(B^{\prime},A^{\prime},0,0)&\text{if
$q_{a}-t_{a}=q_{b}-t_{b}\text{ and }p_{b}\geq p_{a}$}\\\
(b,a,q_{b}-t_{b},p_{a})::f_{u}(B^{\prime},a::A^{\prime},0,t_{a}+q_{b}-t_{b})&\text{if
$q_{a}-t_{a}>q_{b}-t_{b}\text{ and }p_{b}\geq p_{a}$}\\\
(b,a,q_{a}-t_{a},p_{a})::f_{u}(b::B^{\prime},A^{\prime},t_{b}+q_{a}-t_{a},0)&\text{if
$q_{a}-t_{a}<q_{b}-t_{b}\text{ and }p_{b}\geq p_{a}$}\end{cases}$

where $B=b::B^{\prime}$ when $B\neq nil$ and $A=a::A^{\prime}$ when $A\neq
nil$.

_Description_. Observe that, similar to the parameter $t$ in the
$\mathsf{FOB}$ process, we have two parameters $t_{b}$ and $t_{a}$ that inform
the recursive procedure $f_{u}$ that the top bid $b$ and the top ask $a$ have
effective quantities $q_{b}-t_{b}$ and $q_{a}-t_{a}$, respectively. In each
recursive call, the process $f_{u}$ outputs a transaction (top bid $b$, top
ask $a$, quantity $\min\\{q_{b}-t_{b},q_{a}-t_{a}\\}$, price $p_{a}$). The
process $f_{u}$ terminates when the top bid is not matchable with the top ask.

_Remark 1_. It is easy to see that $\mathsf{UM}$ outputs a uniform matching:
Once the $f_{u}$ process terminates, $\mathsf{Last\\_trade\\_price}$ computes
the trade price of the last transaction in the output of $f_{u}$ and
$\mathsf{Replace\\_prices}$ replaces the trade prices of each transaction of
the output of $f_{u}$ with the trade price of the last transaction of the
output, thus ensuring $\mathsf{UM}$ produces a uniform matching. Also, notice
that the process $\mathsf{Replace\\_prices}$ does not alter any other
information of the output of $f_{u}$ apart from the trade prices (we will
later use this fact in the proof of optimality of $\mathsf{UM}$).

_Remark 2_. It is easy to see that $\mathsf{UM}$ outputs an individual-
rational matching: the trade price of a transaction $m$ outputted by a
recursive call of $f_{u}$ is between the limit prices of the bid and the ask
of $m$. Later these prices are altered by $\mathsf{Replace\\_prices}$, but the
individual-rational property is not lost; the trade price of $m$ is also
between the limit prices of the transactions of all the previous calls as the
bids and the asks are sorted by their competitiveness, and
$\mathsf{Replace\\_prices}$ replaces all the trade prices with the trade price
of the last transaction.

Now, we discuss the optimality result of the $\mathsf{UM}$ process. Throughout
this discussion, WLOG, all lists of bids and asks will be sorted by their
competitiveness. We make use of the following notation.

######  Definition 6.2.

Given a matching $M$, a bid $b$ and an ask $a$, we use $Q(a\leftrightarrow
b,M)$ to denote the total traded quantity between the bid $b$ and the ask $a$
in the matching $M$.

Next, we state the main result of this section.

######  Theorem 6.3.

Given a list of bids $B$ and a list of asks $A$, let $M_{U}=\mathsf{UM}(B,A)$
and let $M$ be an arbitrary individual-rational and uniform matching between
$B$ and $A$. Then, $Q(M_{U})\geq Q(M)$. In other words, $\mathsf{UM}$ outputs
an optimal individual-rational-uniform matching.

To prove the above theorem, we need the following lemma.

######  Lemma 6.4.

If $M$ is an individual-rational and uniform matching between the lists of
bids $B=b::B^{\prime}$ and asks $A=a::A^{\prime}$ such that
$Q(M)\geq\min\\{q_{b},q_{a}\\}$, then there exists another individual-rational
and uniform matching $M^{\prime}$ between the same lists of bids $B$ and asks
$A$ such that $Q(M)=Q(M^{\prime})$ and $Q(a\leftrightarrow
b,M^{\prime})=\min\\{q_{b},q_{a}\\}$.

Assuming this lemma, we will first prove Theorem 6.3 and then later prove the
lemma.

_Proof of Theorem 6.3_. Note that $f_{u}(B,A,0,0)$ is a specific instance of
$f_{u}(B,A,t_{b},t_{a})$. So in order to apply the induction hypothesis, we
sensitize the theorem statement to incorporate arbitrary values of $t_{a}$ and
$t_{b}$. Also, as indicated earlier, the $\mathsf{Replace\\_prices}$ function
does not alter the total trade quantity of the output of the $f_{u}$, thus
$Q(f_{u}(B,A,0,0))=Q(\mathsf{UM}(B,A))$. Consequently, showing the following
suffices.

  * ($\ast$)

Fix an arbitrary list of bids $B=b::B^{\prime}$ and an arbitrary list of asks
$A=a::A^{\prime}$. Fix arbitrarily $t_{b}<q_{b}$ and $t_{a}<q_{a}$. Let
$b^{\prime}$ be the bid obtained from the bid $b$ by reducing its quantity to
$q_{b}-t_{b}$. Similarly, let $a^{\prime}$ be the ask obtained from the ask
$a$ by reducing its quantity to $q_{a}-t_{a}$. We will show: for all
individual-rational and uniform matchings $M$ between
$(b^{\prime}::B^{\prime})$ and $(a^{\prime}::A^{\prime})$,
$Q(f_{u}(B,A,t_{b},t_{a}))\geq Q(M)$.

Clearly, setting $t_{b}=t_{a}=0$ in the above statement ($\ast$) gives us
Theorem 6.3.

We prove the above statement using induction on the sum $(|B|+|A|)$. We
consider two cases: $p(b^{\prime})<p(a^{\prime})$ and $p(b^{\prime})\geq
p(a^{\prime})$.

In the first case, when $p(b^{\prime})<p(a^{\prime})$, since the most
competitive bid in $b^{\prime}::B^{\prime}$ is not matchable with the most
competitive ask in $a^{\prime}::A^{\prime}$, any matching between
$b^{\prime}::B^{\prime}$ and $a^{\prime}::A^{\prime}$ is empty. Thus,
$Q(M)=0$, and we are done.

In the second case, when $p(b^{\prime})\geq p(a^{\prime})$, if the total trade
quantity of $M$ is less than the quantity of the transaction created by
$f_{u}$ in the first recursive call (i.e.,
$Q(M)<\min\\{q_{b}-t_{b},q_{a}-t_{a}\\}\leq Q(f_{u}(B,A,t_{b},t_{a})$), then
we are done. In the case when the total traded quantity of $M$ is more than
the quantity of the transaction created by $f_{u}$ in the first recursive call
(i.e., $Q(M)\geq\min\\{q_{b}-t_{b},q_{a}-t_{a}\\}$), we apply Lemma 6.4 and
get another individual-rational and uniform matching $M^{\prime}$ such that
the total volume of $M^{\prime}$ is equal to the total volume of $M$ and the
total traded quantity between the bid $b^{\prime}$ and the ask $a^{\prime}$ in
$M^{\prime}$ is equal to
$\min\\{q_{b^{\prime}}=q_{b}-t_{b},q_{a^{\prime}}=q_{a}-t_{a}\\}$. Now since
we have $M^{\prime}$ such that $Q(M)=Q(M^{\prime})$, proving the following
suffices.

$Q(f_{u}(B,A,t_{b},t_{a}))\geq
Q(M^{\prime})\quad\quad\quad\quad\quad\quad(\ast\ast),$

where $M^{\prime}$ is an individual-rational and uniform matching between the
list of bids $b^{\prime}::B^{\prime}$ and $a^{\prime}::A^{\prime}$ such that
$Q(a^{\prime}\leftrightarrow
b^{\prime},M^{\prime})=\min\\{q_{b}-t_{b},q_{a}-t_{a}\\}$. We define the
matching $M_{0}\subseteq M$ as follows: we remove all transactions between
$b^{\prime}$ and $a^{\prime}$ (of total quantity $Q(a^{\prime}\leftrightarrow
b^{\prime},M^{\prime})$) from $M^{\prime}$ to get $M_{0}$. We have
($\dagger$): $Q(M^{\prime})=\min\\{q_{a}-t_{a},q_{b}-t_{b}\\}+Q(M_{0})$. Also,
note that $M_{0}$ is individual-rational and uniform (since
$M^{\prime}\supseteq M_{0}$ is individual-rational and uniform).

Now we argue the proof of $(\ast\ast)$ in each of the three recursive branches
of the function $f_{u}$ corresponding to $p(b)\geq p(a)$.

  * •

Case: $q_{a}-t_{a}=q_{b}-t_{b}$. In this case $M_{0}$ is a matching between
$B^{\prime}$ and $A^{\prime}$. Since $(|B|+|A|)>(|B^{\prime}|+|A^{\prime}|)$,
we can apply the induction hypothesis to get
$Q(f_{u}(B^{\prime},A^{\prime},0,0))\geq Q(M_{0})$. Now, applying the
definition of $f_{u}$ we get,

$\displaystyle Q(f_{u}(B,A,t_{b},t_{a}))$
$\displaystyle=\min\\{q_{a}-t_{a},q_{b}-t_{b}\\}+Q(f_{u}(B^{\prime},A^{\prime},0,0))$
$\displaystyle\stackrel{{\scriptstyle\text{I.H.}}}{{\geq}}\min\\{q_{a}-t_{a},q_{b}-t_{b}\\}+Q(M_{0})\stackrel{{\scriptstyle(\dagger)}}{{=}}Q(M^{\prime}).$

  * •

Case: $q_{a}-t_{a}>q_{b}-t_{b}$. In this case $M_{0}$ is a matching between
$B^{\prime}$ and $\hat{a}::A^{\prime}$ (where
$q_{\hat{a}}=q_{a}-t_{a}-(q_{b}-t_{b})\leq q_{a}$). Since
$(|B|+|A|)>(|B^{\prime}|+|\hat{a}::A^{\prime}|)$, we can apply the induction
hypothesis when $B^{\prime}\neq\emptyset$ to get
$Q(f_{u}(B^{\prime},A,0,t_{a}+(q_{b}-t_{b})))\geq Q(M_{0})$. When
$B^{\prime}=\emptyset$, then $Q(f_{u}(B^{\prime},A,0,t_{a}+(q_{b}-t_{b})))\geq
Q(M_{0})$ holds trivially as both the sides of the inequality are zeros. Now,
applying the definition of $f_{u}$ we get,

$\displaystyle Q(f_{u}(B,A,t_{b},t_{a}))$
$\displaystyle=(q_{b}-t_{b})+Q(f_{u}(B^{\prime},A,0,t_{a}+(q_{b}-t_{b})))$
$\displaystyle\stackrel{{\scriptstyle\text{I.H.}}}{{\geq}}(q_{b}-t_{b})+Q(M_{0})\stackrel{{\scriptstyle(\dagger)}}{{=}}Q(M^{\prime}).$

  * •

Case: $q_{a}-t_{a}<q_{b}-t_{b}$. This is symmetric to the previous case and
the proof follows similarly. $\square$

Having finished the proof of the main result, we now discuss the proof of the
lemma that we assumed.

_Main proof idea of Lemma 6.4_. Given an individual-rational and uniform
matching $M$ with $Q(M)\geq\min\\{q_{b},q_{a}\\}$ between the list of bids
$B=b::B^{\prime}$ and the list of asks $A=a::A^{\prime}$, we need to show
existence of an individual-rational and uniform matching $M^{\prime}$ such
that $Q(M^{\prime})=Q(M)$ and the total trade quantity between the bid $b$ and
ask $a$ in $M^{\prime}$ is $\min\\{q_{b},q_{a}\\}$. We do the following
surgery on $M$ in two steps to obtain the desired $M^{\prime}$.

Step 1: We first modify $M$ to ensure that bid $b$ and ask $a$ each has at
least $\min\\{q_{b},q_{a}\\}$ total trades in $M$ (not necessarily between
each other). This is accomplished by running the $\mathsf{Fair}$ procedure on
$M$ that outputs a matching which prefers the most competitive orders ($b$ and
$a$) over any other orders. Since $Q(M)\geq\min\\{q_{b},q_{a}\\}$, we get that
$\mathsf{Fair}(M,B,A)$ has at least $\min\\{q_{b},q_{a}\\}$ trades for each of
$b$ and $a$. Note that $\mathsf{Fair}$ does not change the total trade
quantity or affect the individual-rational and uniform properties of $M$. Set
$M\leftarrow\mathsf{Fair}(M,B,A)$.

Step 2: In this step, we modify $M$ to ensure that the bid $b$ and ask $a$
have $\min\\{q_{b},q_{a}\\}$ quantity trade between them. Note that in $M$
individually both $b$ and $a$ have at least $\min\\{q_{b},q_{a}\\}$ total
trade quantity. We will inductively transfer trades of $b$ and $a$ that are
not between them to the transaction between $b$ and $a$, a unit quantity at a
time, till they have $\min\\{q_{b},q_{a}\\}$ quantity trade between them. To
better understand this, consider the case when $b$ and $a$ have zero trade
quantity between them. Let us say there is a transaction between $b$ and
$a_{1}$ of quantity $q_{1}$ and a transaction between $a$ and $b_{1}$ of
quantity $q_{2}$. We remove these two transactions and replace it with the
following four transactions (see Figure 3) that keeps the matching trade
volume intact: (1) transaction between $b$ and $a_{1}$ of quantity $q_{1}-1$,
(2) transaction between $a$ and $b_{1}$ of quantity $q_{2}-1$, (3) transaction
between $b_{1}$ and $a_{1}$ of quantity one and (4) transaction between $b$
and $a$ of quantity one. Recall, in a individual-rational and uniform matching
with price $p$, the limit price of each bid is at least $p$ and the limit
price of each ask is at most $p$, implying any bid and ask participating in
the matching are matchable. Thus, doing such a replacement surgery is legal
and does not affect the individual-rational and uniform properties, and we
obtain the desired $M^{\prime}$ by repeatedly doing this surgery.

$M$$b$$a$$a_{1}$$b_{1}$$q_{2}$$p$$q_{1}$$p$$m_{1}$$m_{2}$$M^{\prime}$$b$$a$$a_{1}$$b_{1}$$q_{2}-1$$p$$q_{1}-1$$p$$b_{1}$$a_{1}$$1$$p$$b$$a$$1$$p$$m_{1}^{\prime}$$m_{2}^{\prime}$$\Rightarrow$

Figure 3:

The proof that $\mathsf{UM}$ produces a fair matching follows from inducting
on the sum $(|A|+|B|)$ and the fact that $B$ and $A$ are sorted by
competitiveness of the participating bids and asks. The argument is similar to
the correctness proof of $\mathsf{Fair}$ that we saw before. From the
discussion above, the next theorem follows immediately.

######  Theorem 6.5.

For a given list of bids $B$ and the list of asks $A$, $M=\mathsf{UM}(B,A)$ is
a fair and optimal individual-rational-uniform matching on $B$ and $A$.

Formalization notes: The formalized proof of the above theorem is done by
first proving Lemma 6.4 (_exists_opt_k_) using induction on the gap
$k=\min\\{q_{b},q_{a}\\}-Q(a\leftrightarrow b,M)$. From this lemma, we get
another matching $M^{\prime}$ such that $Q(a\leftrightarrow
b,M)=\min\\{q_{b},q_{a}\\}$. The matching $M^{\prime}$ is altered to $M_{0}$
(as described in the proof of Theorem 6.3 above) by removing all the
transactions between the bid $b$ and the ask $a$. We prove that the altered
list $M_{0}$ is is a matching between the reduced lists of bids and asks. All
the results related to $M_{0}$ are in the file ’MachingAlter.v’. Finally,
combining all these we prove the main Theorem 6.5 as _’UM_main’_.

##  7 A Maximum Matching Mechanism

In the previous section, we indicated that to achieve maximum trade volume
matching we sometimes have to assign different trade prices to the matched
bid-ask pairs. An individual rational matching with maximum trade volume is
called a maximum matching. In this section we describe a process
$\mathsf{MM}$, that takes a list of bids and a list of asks and outputs a
fair, individual-rational and maximum matching.

The $\mathsf{MM}$ procedure roughly works as follows. In step one, the
$\mathsf{MM}$ procedure repeatedly pairs the most competitive bid $b$ with the
least competitive matchable ask $a$ and outputs a transaction
$(b,a,\min\\{q_{b},q_{a}\\},p_{a})$ and decreases the quantities of $b$ and
$a$ by $\min\\{q_{b},q_{a}\\}$. In step two, the $\mathsf{MM}$ procedure
applies the $\mathsf{Fair}$ procedure on the output of step one.

The detailed $\mathsf{MM}$ procedure and the proof of its correctness are
similar to that of the $\mathsf{UM}$ procedure in spirit. In the proof of
optimality, we need to prove a lemma similar to Lemma 6.4 which states that a
given arbitrary individual-rational matching $M$ of sufficiently large trade
volume can be altered to obtain a matching $M^{\prime}$ of the same total
trade volume such that the total trade quantity between the most competitive
bid and the corresponding least competitive matchable ask in $M^{\prime}$ is
the minimum of their respective quantities. The proof of this requires more
surgeries as compared to that in the proof of Lemma 6.4. Besides this
deviation all other arguments of the proof of optimality of $\mathsf{MM}$ are
similar to that of $\mathsf{UM}$ with minor variations.

The proof of $\mathsf{MM}$ producing an individual-rational matching is
trivial and the proof that it produces a fair matching follows from the fact
that $\mathsf{MM}$ applies the $\mathsf{Fair}$ procedure before it outputs a
final matching. We now state the main theorem of this section.

######  Theorem 7.1.

For a given list of bids $B$ and a list of asks $A$, $\mathsf{MM}(B,A)$ is a
fair, individual-rational and maximum trade volume matching between $B$ and
$A$.

The proof of the above theorem and discussion around the $\mathsf{MM}$
procedure is moved to Appendix C.

Formalization notes: All the formalization details can be found in [1].

##  8 Uniqueness Theorem

In this section, we establish certain theorems that enable us to automatically
check for violations in an exchange matching algorithm by comparing its output
with the output of our certified program. Detailed proofs are available in the
Coq formalization [1].

Ideally, we would have wanted a theorem that the properties (fair and optimal
individual-rational-uniform) imply a unique matching. Such a theorem would
enable us to automatically compare a matching produced by an exchange with a
matching produced by our certified program to find violations of these
properties in the matching produced by the exchange. Unfortunately, such a
theorem is not possible; there exists two different matchings $M_{1}$ and
$M_{2}$ on the same list of bids $B$ and asks $A$, where both are fair and
optimal individual-rational-uniform:
$M_{1}=\\{(b_{1},a_{1},1,p),(b_{2},a_{2},2,p)\\}$ and
$M_{2}=\\{(b_{1},a_{2},1,p),(b_{2},a_{2},1,p),(b_{2},a_{1},1,p)\\}$ on bids
$B=\\{b_{1}=(*,*,1,p),b_{2}=(*,*,2,p)\\}$ and asks
$A=\\{a_{1}=(*,*,1,p),a_{2}=(*,*,2,p)\\}$ for some arbitrary price $p$,
timestamps and ids. Note that fairness does not require the most competitive
bid to be paired with the most competitive ask. For example, assuming $a_{1}$
has a lower timestamp than $a_{2}$ and $b_{1}$ has a lower timestamp than
$b_{2}$ in the above example, $a_{1}$ and $b_{1}$ are not matched in the
matching $M_{2}$, which is a fair matching. Nonetheless, we can show that
given a list of bids $B$ and a list of asks $A$, all matchings that are fair
and individual-rational-uniform, must have the same trade volume for each
trader. This still allows us to automatically check for violations of the
properties in an exchange, by comparing the trades of each trader produced by
the exchange against that produced by our certified program.

We have the following lemma which formulates this uniqueness relation on the
matchings.

######  Theorem 8.1.

Let $M_{1}$ and $M_{2}$ be two fair matchings on the list of bids $B$ and the
list of asks $A$ such that $Q(M_{1})=Q(M_{2})$, then for each order $\omega$,
the total traded quantity of $\omega$ in $M_{1}$ is equal to the total traded
quantity of $\omega$ in $M_{2}$.

_Proof Idea_. We now prove the above theorem by using Lemma 4.6 and deriving a
contradiction. Let $M_{1}$ and $M_{2}$ be fair matchings such that
$Q(M_{1})=Q(M_{2})$. Let $b$ be a buyer whose total trade quantity in $M_{1}$
is different (WLOG, more) from his total trade quantity in $M_{2}$. It is easy
to show that there exists another buyer $b^{\prime}$ such that her total
traded quantity in $M_{1}$ is less than her total traded quantity in $M_{2}$,
i.e., $Q(M_{2},b^{\prime})>Q(M_{1},b^{\prime})$ (since the sum of the total
traded quantities of all the bids of $B$ in $M_{1}$ is equal to the sum of the
total traded quantities of all the bids of $B$ in $M_{2}$ from Lemma 4.6).

Now, there can be two cases: (i) $b$ is more competitive than $b^{\prime}$ or
(ii) $b^{\prime}$ is more competitive than $b$, as per price-time priority. In
the first case, since $Q(M_{1},b)>Q(M_{2},b)$, it follows that
$Q(M_{2},b)<Q(M_{1},b)\leq q_{b}$. This contradicts the fact that $M_{2}$ is
fair on the bids; this is because a less competitive bid $b^{\prime}$ is being
traded in $M_{2}$ (since $Q(M_{2},b^{\prime})>Q(M_{1},b^{\prime})\geq 0$ as
noted above), while a more competitive bid $b$ is not fully traded. Similarly,
in the second case, we show a contradiction to the fact that $M_{1}$ is fair
on the bids. $\hfill\square$

From the above theorem, we have the following corollary.

######  Theorem 8.2.

For any two fair and optimal individual-rational-uniform matchings $M_{1}$ and
$M_{2}$ on the list of bids $B$ and the list of asks $A$, for each order
$\omega$, the total traded quantity of $\omega$ in $M_{1}$ is equal to the
total traded quantity of $\omega$ in $M_{2}$.

For each trader, we can compare the total traded quantities of the trader in
the matching $M_{1}$ produced by an exchange with the total traded quantities
of the trader in the matching $M_{2}=\mathsf{UM}(B,A)$ produced by our
certified program. If for some trader, the traded quantities do not match,
then from Theorem 6.5 and Theorem 8.2 we know that $M_{1}$ does not have the
desired properties as required by the regulators. On the other hand, if they
do match for all traders, then the following theorem states that $M_{1}$ is
fair (Note that uniform and individual-rational properties can be verified
directly from the trade prices and clearly the total trade volume of $M_{1}$
and $M_{2}$ are the same if the traded quantities are same for each trader).

######  Theorem 8.3.

Given a list of bids $B$ and a list of asks $A$, if $M_{1}$ is a fair matching
and $M_{2}$ is an arbitrary matching such that for each order $\omega$, the
total traded quantity of $\omega$ in $M_{1}$ is equal to the total traded
quantity of $\omega$ in $M_{2}$, then $M_{2}$ is fair.

The proof follows immediately from the definition of fairness.

Formalization notes: All the theorems in this section are formalized in the
file ’Uniqueness.v’ using the above proof ideas.

##  9 Demonstration: Automatic Detection of Violations in Real Data

Please see Appendix A for details on our demonstration, where we automate the
process of checking violations in trades using verified programs extracted
from our formalization. We then use this to find violations in trades of 100
stocks traded on a real exchange on a particular day. Below, we describe our
findings.

Out of the 100 stocks we checked, for three stocks our program outputted
"Violation detected!". When we closely examined these stocks, we realized that
in all of these stocks, a market ask order (with limit price = 0), was not
matched by the exchange in its trading output (and these were the only market
ask orders in the entire order-book). On the contrary, market bid orders were
matched by them. With further investigation, we observed that corresponding to
each of these three violations, in the raw data there was an entry of update
request in the order-book with a limit price and timestamp identical to the
uniform price and the auction time, respectively. It seems highly unlikely
that these three update requests were placed by the traders themselves (to
match the microsecond time and also the trade price seems very improbable); we
suspect this is an exchange’s system generated entry in the order-book. We
hope that the exchange is aware of this and doing this consciously. When we
delete the market asks in the preprocessing stage, no violations are detected.
Even if it is not a violation (but a result of the exchange implementing some
unnatural rule that we are not aware of), it is fascinating to see that with
the help of verified programs we can identify such minute and interesting
anomalies which can be helpful for regulating and improving the exchange’s
matching algorithm.

##  10 Related Works and Future Direction

In an earlier work [8], Sarswat and Singh dealt primarily with single unit
trade requests and thus provided a proof of concept for obtaining verified
programs for financial markets. In the current work, we extend their work to
multiple units that results in verified programs which we run on real market
data and establish new uniqueness theorems that enable automatic detection of
violation in exchanges as demonstrated in this work.

Passmore and Ignatovich in [7] highlight the significance, opportunities and
challenges involved in formalizing financial markets. They describe the whole
spectrum of financial algorithms that need to be verified for ensuring safe
and fair markets. Iliano et al. [2] use concurrent linear logic (CLF) to
outline two important properties of a continuous trading system. There are
also some works formalizing various concepts from auction theory [3, 4, 10],
particularly focusing on the Vickrey auction mechanism.

In our opinion, future works should focus on developing a theory for
continuous double auctions for financial markets. Currently the specifications
for continuous double auctions are vague and this is an obstacle for obtaining
verified programs.

## Acknowledgment

We wish to thank Mohit Garg for his generous contribution to this work.

## References

  * [1] Coq formalization of mdsa.  `https://github.com/suneel-sarswat/dsam`.
  * [2] Iliano Cervesato, Sharjeel Khan, Giselle Reis, and Dragisa Zunic.  Formalization of automated trading systems in a concurrent linear framework.  In Linearity-TLLA@FLoC, volume 292 of EPTCS, pages 1–14, 2018\.
  * [3] Cezary Kaliszyk and Julian Parsert.  Formal microeconomic foundations and the first welfare theorem.  In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 91–101. ACM, 2018.
  * [4] Stéphane Le Roux.  Acyclic preferences and existence of sequential nash equilibria: a formal and constructive equivalence.  In International Conference on Theorem Proving in Higher Order Logics, pages 293–309. Springer, 2009.
  * [5] R Preston McAfee.  A dominant strategy double auction.  Journal of economic Theory, 56(2):434–450, 1992.
  * [6] Jinzhong Niu and Simon Parsons.  Maximizing matching in double-sided auctions.  In International conference on Autonomous Agents and Multi-Agent Systems, AAMAS ’13, Saint Paul, MN, USA, May 6-10, 2013, pages 1283–1284, 2013\.
  * [7] Grant Olney Passmore and Denis Ignatovich.  Formal verification of financial algorithms.  In 26th International Conference on Automated Deduction, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 26–41. Springer, 2017.
  * [8] Suneel Sarswat and Abhishek Kr Singh.  Formally verified trades in financial markets.  In Shang-Wei Lin, Zhe Hou, and Brendan Mahoney, editors, Formal Methods and Software Engineering - 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1-3, 2021, Proceedings, volume 12531 of Lecture Notes in Computer Science, pages 217–232. Springer, 2020.
  * [9] Matthieu Sozeau and Cyprien Mangin.  Equations reloaded: High-level dependently-typed functional programming and proving in coq.  Proceedings of the ACM on Programming Languages, 3(ICFP):1–29, 2019\.
  * [10] Emmanuel M. Tadjouddine, Frank Guerin, and Wamberto Weber Vasconcelos.  Abstracting and verifying strategy-proofness for auction mechanisms.  In DALT, volume 5397 of Lecture Notes in Computer Science, pages 197–214. Springer, 2008.
  * [11] Peter R. Wurman, William E. Walsh, and Michael P. Wellman.  Flexible double auctions for electronic commerce: theory and implementation.  Decision Support Systems, 24(1):17–27, 1998.
  * [12] Dengji Zhao, Dongmo Zhang, Md Khan, and Laurent Perrussel.  Maximal matching for double auction.  In Australasian Conference on Artificial Intelligence, volume 6464 of Lecture Notes in Computer Science, pages 516–525. Springer, 2010\.

##  Appendix A Demonstration on real data.

In this section, we demonstrate the practical applicability of our work. For
this, we procured real data from a prominent stock exchange. This data
consists of order-book and trade-book of everyday trading for a certain number
of days. For our demonstration, we considered trades for the top 100 stocks
(as per their market capitalizations) of a particular day. For privacy
reasons, we conceal the real identity of the traders, stocks and the exchange
by masking the stock names (to s1 to s100) and the traders’ identities. We
also converted the timestamps appropriately into natural numbers (which keeps
the time in microseconds, as in the original data). Furthermore, the original
data has multiple requests with the same order id; this is because some
traders update or delete an existing order placed by them before the double
sided auction is conducted. In our preprocessing, we just keep the final lists
of bids and asks in the order-book that participate in the auction.
Furthermore, there are certain market orders, i.e., orders that are ready to
be traded at any available price, which effectively means a limit price of
zero for an ask and a limit price of infinity for a bid; in the preprocessing
we set these limit prices to zero and the largest OCaml integer, respectively.

We then extracted the verified OCaml programs and ran them on the processed
market data. The output trades of the verified code were then compared with
the actual trades in the trade-book from the exchange. From the uniqueness
theorems in the Section 8, we know that if the total trade quantity of each
order in these two matchings are equal, then the matching produced by the
exchange has the desired properties (if it is uniform and IR which can be
checked trivially by looking at the prices in the trade-book). We also know
that if they are not equal for some trader, then the matching algorithm of the
exchange does not have the requisite desired properties (or there is some
error in storing or reporting the order-book or the trade-book accurately).

The processed data and the relevant programs for this demonstration are
available at [1]. The extracted OCaml programs of the functions required for
this demonstration are stored in a separate file named ‘certified.ml’. The
input bids, asks and trades of each stock are in ‘s.bid’, ‘s.ask’ and
‘s.trade’ files, where ‘s’ is the masked id for that stock. For example, file
‘s1.bid’ contains all the bids for the stock ‘s1’. To feed the inputs to the
verified program and to print the output of the certified program, we have
written two OCaml scripts: create.ml and compare.ml. The create.ml script
feeds inputs (lists of bids and asks) to the UM process, and then prints its
output matching $M$. The compare.ml script compares the matching produced by
the UM process $M$ with the actual trades $M_{\text{EX}}$ in the exchange
trade-book. If the total trade quantity for all the traders in $M$ matches
with that of the total trade quantity in $M_{\text{EX}}$, then the compare.ml
script outputs "Matching does not violate the guidelines". If for some bid (or
ask) the total trade quantity of $M$ and $M_{\text{EX}}$ does not match, then
the program outputs "Violation detected!".

##  Appendix B Proof details for Theorem 5.5.

For a given matching $M$ on the list of bids $B$ and the list of asks $A$, we
prove the main theorem by broadly establishing the following properties.

  1. 1.

$\text{For all }m\in f(M,B,0),\ p(a_{m})\leq p(b_{m})$.

  2. 2.

$B_{f(M,B,t)}\subseteq B$.

  3. 3.

$A_{f(M,B,t)}\subseteq A_{M}$.

  4. 4.

$\text{For all }b\in B_{f(M,B,t)},\ Q(b,f(M,B,t))\leq q_{b}$.

  5. 5.

$\text{For all }a\in A_{f(M,B,t)},\ Q(a,f(M,B,t))\leq q_{a}$.

  6. 6.

$\text{For all }a\in A_{M},\ Q(a,f(M,B,0))=Q(a,M)$.

  7. 7.

$\text{For all }a\in A_{M},\text{ if }Q(B)\geq Q(M)+t\text{, then
}Q(a,M)=Q(a,f(M,B,t))$.

  8. 8.

$\text{For all }b_{1},b_{2}\in B_{f(M,B,0)},\text{ if }b_{1}\text{ is more
competitive than }b_{2}\text{, then }Q(b_{1},f(M,B,0))=q(b_{1})$.

  9. 9.

$\text{For all }b_{1},b_{2}\in B_{f(M,B,t)},\text{ if }b_{1}\text{ is more
competitive than }b_{2}\text{, then }Q(M)>(q_{b_{1}}-t)$.

  10. 10.

$\text{If }Q(M)\geq(q_{b}-t)\text{, then }Q(b,f(M,b::B,t))=(q_{b}-t)$.

Observe that, the $\mathsf{FOB}$ procedure calls subroutine $f$ with $t=0$.
However, if we try to prove the properties of $\mathsf{FOB}$ using induction
while fixing $t=0$, we get a weaker induction hypothesis. This is because in
one of the recursive cases, the value of $t$ is not zero. On the other hand,
some results holds true only for $t=0$. Therefore, it is helpful to separately
prove the results essential for the main theorem and identify how the
correctness of each of these results is sensitive to the different values of
$t$

In the above list of properties, (1) - (5) are needed to prove that
$M_{\beta}$ is matching and are closely linked to the five properties of
Definition 4.4. Observe that while the properties (2) - (5) are true for
arbitrary values of $t$, property (1) is special case with term $t=0$. The
property (1) above says that all the bid-ask pairs produced by $f$ are
matchable only when the function $f$ is called with $t=0$. For see this,
consider the function call $f(m::M^{\prime},b::B^{\prime},q_{b})$ with
$t=q_{b}$. Also assume that none of the bids of $B^{\prime}$ is matchable with
the ask of $m$(i.e., $\forall b^{\prime}\in
B^{\prime},p(b^{\prime})<p(a_{m})$). In this case the most competitive bid $b$
is already fully traded, as indicated by $t$, and hence the function $f$ will
try to match $a_{m}$ with some other $b^{\prime}\in B^{\prime}$, which will
not be matchable.

By substituting $t=0$ in (7), we can prove property (6) which states that
function $\mathsf{FOB}$ does not change the filled quantity for any ask $a$
appearing in the original matching $M$. Similarly, by using properties (9) and
(10) we can prove property (8) above, which states that a more competitive bid
$b_{1}$ is fully traded before starting any transaction involving a less
competitive bid $b_{2}$. Also note that similar to earlier, property (8) is
only true for $t=0$, the properties (9) and (10) are statements about the
properties of $f(M,B,t)$ for an arbitrary $t$.

##  Appendix C A Maximum Matching Mechanism

In Section 6, we noted that to obtain a maximum matching on certain inputs we
may have to compromise the uniform properties. We now describe a matching
mechanism which produces a maximum trade volume matching. We can then use the
function $\mathsf{FOA}$ to make it fair.

######  Definition C.1.

Maximum Matching ($\mathsf{MM}$).

$\displaystyle\mathsf{MM}(B,A)=\mathsf{FOA}(\stackrel{{\scriptstyle\mathbb{A}}}{{\uparrow}}f_{m}(\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}B,\stackrel{{\scriptstyle\mathbb{A}}}{{\downarrow}}A,0,0),\stackrel{{\scriptstyle\mathbb{A}}}{{\uparrow}}A)$
$\displaystyle\text{where }f_{m}(B,A,t_{b},t_{a})=$
$\displaystyle\begin{cases}nil&\text{if $B=nil$ or $A=nil$}\\\
f(b::B^{\prime},A^{\prime},t_{b},0)&\text{if $p_{b}<p_{a}$}\\\
(b,a,q_{a}-t_{a},p_{a})::f_{m}(B^{\prime},A^{\prime},0,0)&\text{if
$q_{a}-t_{a}=q_{b}-t_{b}\text{ and }p_{b}\geq p_{a}$}\\\
(b,a,q_{a}-t_{a},p_{a})::f_{m}(b::B^{\prime},A^{\prime},q_{b}+q_{a}-t_{a},0)&\text{if
$q_{a}-t_{a}<q_{b}-t_{b}\text{ and }p_{b}\geq p_{a}$}\\\
(b,a,q_{b}-t_{b},p_{a})::f_{m}(B^{\prime},a::A^{\prime},0,q_{a}+q_{b}-t_{a})&\text{if
$q_{a}-t_{a}>q_{b}-t_{b}\text{ and }p_{b}\geq p_{a}$}\end{cases}$

where $B=b::B^{\prime}$ when $B\neq nil$ and $A=a::A^{\prime}$ when $A\neq
nil$.

_Description_. Procedure $\mathsf{MM}(B,A)$ first sorts the list of bids $B$
in decreasing order of their competitiveness and the list of asks $A$ in
increasing order of their competitiveness and calls the $f_{m}$ procedure on
these sorted lists. Similar to $\mathsf{UM}$ procedure, we use parameters
$t_{b}$ and $t_{a}$ that inform the recursive procedure $f_{m}$ that the top
bid $b$ and the top ask $a$ have effective quantities $q_{b}-t_{b}$ and
$q_{a}-t_{a}$, respectively. In each iteration, the function $f_{m}$ first
check if the most competitive bid $b$ is matchable to the least competitive
ask $a$; If they are matchable (i.e $p_{b}\geq p_{a}$), then a transaction
between $b$ and $a$ with quantity $q=\min\\{q_{b}-t_{b},q_{a}-t_{a}\\}$ and
price $p_{a}$ is created and the function recursively proceeds on smaller
inputs by appropriately updating the filled trade quantities of the top bid
and ask; If $b$ and $a$ are not matchable (i.e. $p_{b}<p_{a}$) the function
ignores the current ask $a$ and proceeds recursively on smaller input. If
either of the lists $B$ or $A$ becomes nil, the function $f_{m}$ terminates
and outputs a matching between the lists of bids $B$ and asks $A$.

_Remark_. The function $f_{m}$ always tries to match the unfilled trade
quantities of the most competitive bid $b$ in $B$ against the unfilled
quantities of the first matchable least competitive ask in $A$. It is
important to note that due to this difference in operation, now we cannot
claim that in each successive recursive call of $f_{m}$, when it outputs a
transaction, the trade price assigned by it (i.e. $p_{a}$) is greater than or
equal to the limit prices of all the asks paired so far (due to the reversed
order or sorting of $A$). Hence, unlike $\mathsf{UM}$ process we are not sure
about the possibility of finding a common price that can be used to make it
uniform as well as individual-rational simultaneously. Moreover, the procedure
$f_{m}$ outputs a fair on bids matching, it might not be fair on asks.
Therefore, the procedure $\mathsf{MM}$ calls the procedure $\mathsf{FOA}$ on
the output of $f_{m}$ and the lists of asks $A$ (now, sorted in decreasing
order of their competitiveness). As a result, $\mathsf{MM}$ outputs a fair
matching on the lists of bids $B$ and the asks $A$.

We now discuss some important results leading to the main theorem of this
section which states that for an arbitrary list of bids $B$ and list of asks
$A$, where $B$ is sorted by decreasing order of the competitiveness while $A$
is sorted in increasing order of the competitiveness, the function $f_{m}$
produces a matching which is maximum by trade volume among all the matchings
on $B$ and $A$.

######  Lemma C.2.

If $M$ is a matching on the list of bids
$B=\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}(b::B^{\prime})$ and the
list of asks
$A=\stackrel{{\scriptstyle\mathbb{A}}}{{\downarrow}}(a::A^{\prime})$, and
$Q(M)\geq q$, where $q=\min\\{q_{b},q_{a}\\}$, then there exists a matching
$M^{\prime}$ on $B$ and $A$, with $Q(M^{\prime})=Q(M)$ and
$Q(b,M^{\prime})\geq q$.

_Proof Idea_. For the given $M$, $B$ and $A$ consider
$M^{\prime}=\mathsf{FOB}(\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}M,\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}b::B^{\prime})$.
Since $\mathsf{FOB}$ does not change the overall trade volume we have
$Q(M^{\prime})\geq q$. Now since $M^{\prime}$ is fair on bids with total trade
volume higher than the available quota $q$ of both $a$ and $b$, it must fill
at least $q$ quantity of $b$ before trading the other less competitive bids
from $B^{\prime}$. Hence, we have $Q(b,M^{\prime})\geq q$. $\square$

######  Lemma C.3.

If $M^{\prime}$ is a matching on the list of bids
$B=\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}(b::B^{\prime})$ and the
list of asks
$A=\stackrel{{\scriptstyle\mathbb{A}}}{{\downarrow}}(a::A^{\prime})$, with
$p_{b}\geq p_{a}$ and $Q(b,M^{\prime})\geq q$, where
$q=\min\\{q_{b},q_{a}\\}$, then there exists a matching $M^{\prime\prime}$ on
$B$ and $A$, with $Q(M^{\prime\prime})=Q(M^{\prime})$ and $Q(a\leftrightarrow
b,M^{\prime\prime})=q$.

_Proof Idea_. Note that while the term $Q(a\leftrightarrow
b,M^{\prime\prime})$ represents the total volume of trade between $b$ and $a$
in $M^{\prime\prime}$, the quantity $q$ represents the maximum possible trade
between $b$ and $a$ in any arbitrary matching $M$ provided $p_{b}\geq p_{a}$.
Now assume that we have $Q(a\leftrightarrow b,M^{\prime})=q-k$, where $k$
represents the trade deficit between $b$ and $a$ particular to $M^{\prime}$.
The existence of a matching $M^{\prime\prime}$ with no trade deficit can be
shown using mathematical induction on the value of $k$. Again, at the core of
this inductive argument is a method by which we generate another matching
$M_{1}$ from $M^{\prime}$ with same trade volume while reducing the trade
deficit among $a$ and $b$ by one unit. We now consider the following two
possibilities (1) $Q(a,M^{\prime})<q$, and (2) $Q(a,M^{\prime})\geq q$. In the
case (1) if $k>0$ we can prove that $\exists m\in
M^{\prime},m=(b,a_{1},q_{1},p_{m})$, where $a_{1}\neq a$. Now consider
$M_{1}=(b,a,1,p_{a})::M^{\prime}[m\mapsto m^{\prime}]$, where
$m^{\prime}=(b,a_{1},q_{1}-1,p_{m})$ (see Figure 4). It is easy to see that
$M_{1}$ is a matching with $Q(a\leftrightarrow b,M_{1})=q-k-1$ while
$Q(M_{1})=Q(M^{\prime})$. In the case (2), where $Q(a,M^{\prime})\geq q$, if
$k>0$ then it can be shown that $\exists\;m_{1}\;m_{2}\in
M^{\prime},m_{1}=(b,a_{1},q_{1},p_{1})\text{ and
}m_{2}=(b_{1},a,q_{2},p_{2})$, where $b\neq b_{1}$ and $a\neq a_{1}$.
Moreover, since
$\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}b::B^{\prime}$,
$\stackrel{{\scriptstyle\mathbb{A}}}{{\downarrow}}a::A^{\prime}$, and $m_{1}$
and $m_{2}$ are valid transactions we can conclude that $p_{b}\geq
p(b_{1})\geq p_{a}\geq p(a_{1})$. Furthermore, we define
$M_{1}=(b,a,1,p_{a})::(b_{1},a_{1},1,p(a_{1}))::M^{\prime}[m_{1}\mapsto
m_{1}^{\prime},m_{2}\mapsto m_{2}^{\prime}]$, where
$m_{1}^{\prime}=(b,a_{1},q_{1}-1,p_{1})$ and
$m_{2}^{\prime}=(b_{1},a,q_{2}-1,p_{2})$. Note that $Q(a\leftrightarrow
b,M_{1})=q-k-1$ while $Q(M_{1})=Q(M^{\prime})$. This process can be repeated
to get a $M^{\prime\prime}$ where the trade deficit is zero (i.e.
$Q(a\leftrightarrow b,M^{\prime\prime})=q$). $\square$

$M^{\prime}$$a_{1}$$b$$q_{1}$$p_{m}$$m$$M_{1}$$a_{1}$$b$$q_{1}-1$$p_{m}$$b$$a$$1$$p_{a}$$m^{\prime}$$\Rightarrow$

Figure 4: In the above figure the matching $M_{1}$ is obtained from the
matching $M^{\prime}$. Total trade volume in both $M^{\prime}$ and $M_{1}$ is
equal. Furthermore, the trade quantity between $a$ and $b$ in $M_{1}$ is one
more than that in $M^{\prime}$.

######  Theorem C.4.

Let $M$ be an arbitrary matching on the given list of bids $B$ and list of
asks $A$, and $M_{m}=f_{m}(\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow
B}},\stackrel{{\scriptstyle\mathbb{A}}}{{\downarrow}}A,0,0)$ then $M_{m}$ is a
matching on $B$ and $A$ with $Q(M_{m})\geq Q(M)$.

_Proof Outline_. The proof of this theorem is using induction on the sum
$(|B|+|A|)$, however due to the reasons similar in the proof of Theorem 6.3 we
prove this theorem by proving the following claim which incorporates the
changing values of $t_{a}$ and $t_{b}$.

  * •

$\forall M,\text{Matching
}M\;((id_{b},\tau_{b},q_{b}-t_{b},p_{b})::B)\;((id_{a},\tau_{a},q_{a}-t_{a},p_{a})::A)\rightarrow
Q(f_{m}(\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}b::B,\stackrel{{\scriptstyle\mathbb{A}}}{{\downarrow}}a::A,t_{b},t_{a}))\geq
Q(M)$

We prove this result using induction on the value $(|b::B|+|a::A|)$, and
unfolding the definition of $f_{m}$ in each branch of the computation. We get
the following induction hypothesis (IH), where $B^{\prime}_{-t_{b}}$ and
$A^{\prime}_{-t_{a}}$ are the list of bids and list of asks obtained after
updating the unfilled quotas of the top bid and top ask as per the values of
$t_{b}$ and $t_{a}$ respectively.

  * •

IH:
$\forall\;B^{\prime}\;A^{\prime}\;t_{a}\;t_{b}\;M_{0},\,|B^{\prime}|+|A^{\prime}|<|b::B|+|a::A|\rightarrow(\text{Matching}\;M_{0}\;B^{\prime}_{-t_{b}}A^{\prime}_{-t_{a}}\\\
\rightarrow Q(f_{m}(\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow
B^{\prime}}},\stackrel{{\scriptstyle\mathbb{A}}}{{\downarrow
A^{\prime}}},t_{b},t_{a}))\geq Q(M_{0}))$

We first consider the case when $p_{b}<p_{a}$. In this case
$f_{m}(b::B,a::A,t_{b},t_{a})$ reduces to $f_{m}(b::B,A,t_{b},0)$ and hence
produces a matching on $b::B$ and $A$. Moreover, since $p_{a}>p_{b}$ the ask
$a$ cannot participate in any matching between $b::B$ and $a::A$. Hence we can
conclude that $M$ is also a matching between $b::B$ and $A$. Therefore using
induction hypothesis we have
$Q(f_{m}(\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}b::B,\stackrel{{\scriptstyle\mathbb{A}}}{{\downarrow}}a::A,t_{b},t_{a}))=Q(f_{m}(\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}b::B,\stackrel{{\scriptstyle\mathbb{A}}}{{\downarrow}}A,t_{b},0))\geq
Q(M)$, which proves the result in this case. Now consider the case when $a$
and $b$ are matchable (i.e. $p_{b}\geq p_{a}$). Let
$q=\min\\{q_{b}-t_{b},q_{a}-t_{a}\\}$, and $Q(M)<q$. In this case, the theorem
statement is true since our algorithm produces a matching of total trade
volume greater than or equal to $q$. Now consider the second case when
$Q(M)\geq q$. In this case, using Lemma C.2 and Lemma C.3, we prove that there
exists a matching $M^{\prime\prime}$ between the list of bids
$(id_{b},\tau_{b},q_{b}-t_{b},p_{b})::B$ and the list of asks
$(id_{a},\tau_{a},q_{a}-t_{a},p_{a})::A$, such that $Q(M^{\prime\prime})=Q(M)$
and $Q(a\leftrightarrow b,M^{\prime\prime})=q$. Note that we now have a
matching $M^{\prime\prime}$ with the same total trade volume as $M$ but having
maximum possible trade between the top bid $b$ and top ask $a$. Therefore, we
complete the proof of this theorem by proving
$Q(f_{m}(\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}b::B,\stackrel{{\scriptstyle\mathbb{A}}}{{\downarrow}}a::A,t_{b},t_{a}))\geq
Q(M^{\prime\prime})$. We now prove this result in each of the following three
cases.

$\triangleright$ _C 1_. In this case, when $q_{a}-t_{a}=q_{b}-t_{b}$, we have
$Q(f_{m}(\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}b::B,\stackrel{{\scriptstyle\mathbb{A}}}{{\downarrow}}a::A,t_{b},t_{a}))=q+Q(f_{m}(B,A,0,0))\geq
q+Q(M_{0})=Q(M^{\prime\prime})$, where $M_{0}$ is a matching between $B$ and
$A$. Note that we can claim $q+Q(f_{m}(B,A,0,0))\geq q+Q(M_{0})$ since
$Q(f_{m}(B,A,0,0))\geq Q(M_{0})$ from the induction hypothesis.

$\triangleright$ _C 2_. In this case $q_{a}-t_{a}>q_{b}-t_{b}$, and we have
$Q(f_{m}\stackrel{{\scriptstyle\mathbb{B}}}{{(\uparrow}}b::B,\stackrel{{\scriptstyle\mathbb{A}}}{{\downarrow}}a::A,t_{b},t_{a}))=q+Q(f_{m}(B,a::A,0,t_{a}+q_{b}-t_{b}))\geq
q+Q(M_{0})=Q(M^{\prime\prime})$, where $M_{0}$ is a matching between $B$ and
$(id_{a},\tau_{a},(q_{a}-t_{a}-(q_{b}-t_{b})),p_{a})::A$. Note that in this
case $q=(q_{b}-t_{b})$ and again we can claim
$q+Q(f_{m}(B,a::A,0,t_{a}+q_{b}-t_{b}))\geq q+Q(M_{0})$ because we know
$Q(f_{m}(B,a::A,0,t_{a}+q_{b}-t_{b}))\geq Q(M_{0})$ from the induction
hypothesis.

$\triangleright$ _C 3_. In this case $q_{a}-t_{a}<q_{b}-t_{b}$ and we have
$Q(f_{m}(\stackrel{{\scriptstyle\mathbb{B}}}{{\uparrow}}b::B,\stackrel{{\scriptstyle\mathbb{A}}}{{\downarrow}}a::A,t_{b},t_{a}))=q+Q(f_{m}(b::B,A,t_{b}+q_{a}-t_{a},0))\geq
q+Q(M_{0})=Q(M^{\prime\prime})$, where $M_{0}$ is a matching between
$(id_{b},\tau_{b},(q_{b}-t_{b}-(q_{a}-t_{a})),p_{b})::B$ and $A$. Again in
this case $q+Q(f_{m}(b::B,A,t_{b}+q_{a}-t_{a},0))\geq q+Q(M_{0})$ follows from
$Q(f_{m}(b::B,A,t_{b}+q_{a}-t_{a},0))\geq Q(M_{0})$ from the induction
hypothesis. $\square$

######  Theorem C.5.

For a given list of bids $B$ and the list of asks $A$, $M=\mathsf{MM}(B,A)$ is
a fair, individual-rational and maximum volume matching on $B$ and $A$.