A Certified Pointer-Style SSA Data Structure

Intermediate representations in static single assignment (SSA) form offer local reasoning, fast direct access, and intuitive algorithms, which has made them the de facto standard in industrial compilers. While assigning each variable exactly once is the name-giving concept behind SSA, its true power is the underlying data structure that ensures fast asymptotic and absolute performance. Yet, instead of using a fast SSA data structure, certified compilers either do not use SSA, or formalize SSA without efficient implementations. High-performance pointer-heavy graph data structures such as SSA have, in general, never been implemented inside a theorem prover. We implement an asymptotically-fast SSA data structure in the Lean functional language and theorem prover. We closely mirror LLVM and MLIR, both widely used to compile general-purpose programming languages and DSLs, in data structure design and API. We establish the internal invariants and the functional correctness of key operations of this graph data structure, using a layered strategy designed to leverage Lean's automation. We demonstrate usability and performance by building an MLIR parser, rewriter, and block inliner. This work provides the missing link between the rigorous guarantees of formal methods and the performance expectations of modern, large-scale compiler frameworks.