Tail Modulo Cons, OCaml, and Relational Separation Logic

TL;DR

This paper addresses stack-space concerns for recursive functions in OCaml by proposing Tail Modulo Cons (TMC), an on-demand transformation that makes data-constructing recursive functions like List.map tail-recursive and stack-safe. The core approach includes implementing TMC in the OCaml compiler, along with a mechanized correctness proof for a simplified untyped calculus using relational Iris logic, and extending Simuliris to handle different calling conventions. The main contributions are the OCaml-compiler integration of TMC, a formal, machine-checked justification of its correctness, and a generalized framework for simulation-based verification of compiler transformations. The work has practical impact by enabling efficient, easy-to-write tail-recursive code and advancing verification techniques for compiler optimizations via Iris and Simuliris.

Abstract

Common functional languages incentivize tail-recursive functions, as opposed to general recursive functions that consume stack space and may not scale to large inputs. This distinction occasionally requires writing functions in a tail-recursive style that may be more complex and slower than the natural, non-tail-recursive definition. This work describes our implementation of the *tail modulo constructor* (TMC) transformation in the OCaml compiler, an optimization that provides stack-efficiency for a larger class of functions -- tail-recursive *modulo constructors* -- which includes in particular the natural definition of `List.map` and many similar recursive data-constructing functions. We prove the correctness of this program transformation in a simplified setting -- a small untyped calculus -- that captures the salient aspects of the OCaml implementation. Our proof is mechanized in the Coq proof assistant, using the Iris base logic. An independent contribution of our work is an extension of the Simuliris approach to define simulation relations that support different calling conventions. To our knowledge, this is the first use of Simuliris to prove the correctness of a compiler transformation.