Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Double Auctions: Formalization and Automated Checkers

Mohit Garg, N. Raja, Suneel Sarswat, Abhishek Kr Singh

TL;DR

This work establishes new uniqueness theorems, enabling automatic detection of violations in exchange systems by comparing their output to that of a verified program, and extracts verified OCaml and Haskell programs that could serve as a resource for exchanges and market regulators.

Abstract

Double auctions are widely used in financial markets, such as those for stocks, derivatives, currencies, and commodities, to match demand and supply. Once all buyers and sellers have placed their trade requests, the exchange determines how these requests are to be matched. The two most common objectives for determining the matching are maximizing trade volume at a uniform price and maximizing trade volume through dynamic pricing. Prior research has primarily focused on single-quantity trade requests. In this work, we extend the framework to handle multiple-quantity trade requests and present fully formalized matching algorithms for double auctions, along with their correctness proofs. We establish new uniqueness theorems, enabling automatic detection of violations in exchange systems by comparing their output to that of a verified program. All proofs are formalized in the Coq Proof Assistant, and we extract verified OCaml and Haskell programs that could serve as a resource for exchanges and market regulators. 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.

Double Auctions: Formalization and Automated Checkers

TL;DR

This work establishes new uniqueness theorems, enabling automatic detection of violations in exchange systems by comparing their output to that of a verified program, and extracts verified OCaml and Haskell programs that could serve as a resource for exchanges and market regulators.

Abstract

Double auctions are widely used in financial markets, such as those for stocks, derivatives, currencies, and commodities, to match demand and supply. Once all buyers and sellers have placed their trade requests, the exchange determines how these requests are to be matched. The two most common objectives for determining the matching are maximizing trade volume at a uniform price and maximizing trade volume through dynamic pricing. Prior research has primarily focused on single-quantity trade requests. In this work, we extend the framework to handle multiple-quantity trade requests and present fully formalized matching algorithms for double auctions, along with their correctness proofs. We establish new uniqueness theorems, enabling automatic detection of violations in exchange systems by comparing their output to that of a verified program. All proofs are formalized in the Coq Proof Assistant, and we extract verified OCaml and Haskell programs that could serve as a resource for exchanges and market regulators. 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.

Paper Structure

This paper contains 16 sections, 16 theorems, 18 equations, 2 figures, 5 algorithms.

Table of Contents

  1. Introduction
  2. Overview of Double Auctions
  3. Our Contributions
  4. Related Work
  5. Preliminaries
  6. Orders
  7. Transactions and Matchings
  8. Classes of Matchings
  9. Demand-Supply Inequality
  10. The $\mathsf{Fair}$ Algorithm
  11. Fair on Asks
  12. Matching Algorithms
  13. Optimal-Uniform Matching Algorithm
  14. Maximum Matching Algorithm
  15. Uniqueness Theorems and Automated Checkers
  16. ...and 1 more sections

Key Result

Theorem 6

If $M$ is a matching over an admissible order-domain $(B, A)$, then for all natural numbers $p$, we have $\mathsf{Vol}(M) \leq \mathsf{Vol}(B_{\geq p}) + \mathsf{Vol}(A_{\leq p})$.

Figures (2)

  • Figure 1: Sometimes to maximize the total trade volume, we have to accept different trade prices to the matched bid-ask pairs. In this example the only matching of size two is not uniform. Here the bids (B) and the asks (A) all have quantity one each, and their limit prices are displayed.
  • Figure 2: In the above figure the matching $M'$ is obtained from the matching $M$. Each bid or ask has the same trade quantity in both $M$ and $M'$. Furthermore, the trade quantity between $a$ and $b$ in $M'$ is one more than that in $M$.

Theorems & Definitions (26)

  • Remark
  • Theorem 6: Demand-Supply Inequality
  • proof : Proof of \ref{['thm:boundM']}
  • Theorem 7
  • proof : Proof of \ref{['thm:FOA']}
  • Claim
  • Remark
  • Theorem 7: Correctness of $\Fair$
  • Proposition 8
  • Proposition 9
  • ...and 16 more