Implementing hash-consed structures in Coq

TL;DR

This paper explores three methods for integrating hash-consed structures into Coq-certified programs, analyzing their performance and guarantees in different execution contexts, using BDDs as a case study.

Contribution

It introduces and compares three approaches for hash-consing in Coq, highlighting their trade-offs and implications for certified program execution and extraction.

Findings

Different approaches offer trade-offs between performance and fidelity to Coq code.

Execution inside Coq and in extracted OCaml code vary in efficiency and guarantees.

Fine-tuning OCaml code can improve performance but may affect certification guarantees.

Abstract

We report on three different approaches to use hash-consing in programs certified with the Coq system, using binary decision diagrams (BDD) as running example. The use cases include execution inside Coq, or execution of the extracted OCaml code. There are different trade-offs between faithful use of pristine extracted code, and code that is fine-tuned to make use of OCaml programming constructs not available in Coq. We discuss the possible consequences in terms of performances and guarantees.