Continuous double auctions are commonly used to match orders at currency, stock, and commodities exchanges. A verified implementation of continuous double auctions is a useful tool for market regulators as they give rise to automated checkers that are guaranteed to detect errors in the trade logs of an existing exchange if they contain trades that violate the matching rules. We provide an efficient and formally verified implementation of continuous double auctions that takes $O(n \log n)$ time to match $n$ orders. This improves an earlier $O(n^2)$ verified implementation. We also prove a matching $\Omega(n\log n)$ lower bound on the running time for continuous double auctions. Our new implementation takes only a couple of minutes to run on ten million randomly generated orders as opposed to a few days taken by the earlier implementation. Our new implementation gives rise to an efficient automatic checker. We use the Coq proof assistant for verifying our implementation and extracting a verified OCaml program. While using Coq's standard library implementation of red-black trees to obtain our improvement, we observed that its specification has serious gaps, which we fill in this work; this might be of independent interest.

翻译：连续双向拍卖常用于货币、股票及商品交易所的订单匹配。对于市场监管机构而言，可验证的连续双向拍卖实现是一个实用工具，因为它能生成自动化检查器，当现有交易所的交易日志中包含违反匹配规则的交易时，该检查器可保证检测出其中的错误。我们提出了一种高效且经过形式化验证的连续双向拍卖实现，其匹配n个订单的时间复杂度为$O(n \log n)$，这改进了先前$O(n^2)$的验证实现。我们还证明了连续双向拍卖运行时间的匹配下界为$\Omega(n\log n)$。新实现处理一千万个随机生成订单仅需数分钟，而先前实现则需要数天。新实现可生成高效的自动化检查器。我们使用Coq证明辅助工具验证实现并提取出可验证的OCaml程序。在利用Coq标准库的红黑树实现以获得性能改进时，我们发现其规范存在重大缺陷，我们在本工作中进行了填补；这可能具有独立的研究价值。