A Verified Cost Analysis of Joinable Red-Black Trees

TL;DR

This paper presents a formally verified implementation and cost analysis of joinable red-black trees within a dependently typed framework, ensuring correctness and precise operation bounds for sequence algorithms.

Contribution

It introduces a verified, cost-analyzed implementation of joinable red-black trees in calf, maintaining invariants and bounding operation costs within a formal proof system.

Findings

Verified cost bounds for red-black tree operations

Mechanized proofs in Agda ensure correctness invariants

Implementation supports efficient sequence algorithms

Abstract

Ordered sequences of data, specified with a join operation to combine sequences, serve as a foundation for the implementation of parallel functional algorithms. This abstract data type can be elegantly and efficiently implemented using balanced binary trees, where a join operation is provided to combine two trees and rebalance as necessary. In this work, we present a verified implementation and cost analysis of joinable red-black trees in $\textbf{calf}$, a dependent type theory for cost analysis. We implement red-black trees and auxiliary intermediate data structures in such a way that all correctness invariants are intrinsically maintained. Then, we describe and verify precise cost bounds on the operations, making use of the red-black tree invariants. Finally, we implement standard algorithms on sequences using the simple join-based signature and bound their cost in the case that red-black trees are used as the underlying implementation. All proofs are formally mechanized using the embedding of $\textbf{calf}$ in the Agda theorem prover.