Complete first-order reasoning for functional programs
Provides foundational theoretical justification for a widely used verification heuristic, clarifying its completeness and limitations for program verifiers.
The paper proves that the heuristic of unrolling recursive function definitions followed by quantifier-free SMT reasoning is complete for first-order reasoning over algebraic datatypes with decidable background theories, explaining the success and failure modes of tools like Liquid Haskell and Leon.
Several practical tools for automatically verifying functional programs (e.g., Liquid Haskell and Leon for Scala programs) rely on a heuristic based on unrolling recursive function definitions followed by quantifier-free reasoning using SMT solvers. We uncover foundational theoretical properties of this heuristic, revealing that it can be generalized and formalized as a technique that is in fact complete for reasoning with combined First-Order theories of algebraic datatypes and background theories, where background theories support decidable quantifier-free reasoning. The theory developed in this paper explains the efficacy of these heuristics when they succeed, explains why they fail when they fail, and the precise role that user help plays in making proofs succeed.