The Search for Constrained Random Generators

TL;DR

This paper introduces a novel, deductive synthesis-based approach for efficiently generating constrained random test values in property-based testing, implemented in the Palamedes library for Lean.

Contribution

It presents a new synthesis method for constrained generators using denotational semantics, simplifying recursive predicate handling and integrating with Lean proof automation.

Findings

The approach effectively handles recursive predicates via rewriting as catamorphisms.

The implementation, Palamedes, is an extensible Lean library utilizing proof-search tactics.

The method improves efficiency in generating valid test cases for property-based testing.

Abstract

Among the biggest challenges in property-based testing (PBT) is the constrained random generation problem: given a predicate on program values, randomly sample from the set of all values satisfying that predicate, and only those values. Efficient solutions to this problem are critical, since the executable specifications used by PBT often have preconditions that input values must satisfy in order to be valid test cases, and satisfying values are often sparsely distributed. We propose a novel approach to this problem using ideas from deductive program synthesis. We present a set of synthesis rules, based on a denotational semantics of generators, that give rise to an automatic procedure for synthesizing correct generators. Our system handles recursive predicates by rewriting them as catamorphisms and then matching with appropriate anamorphisms; this is theoretically simpler than other approaches to synthesis for recursive functions, yet still extremely expressive. Our implementation, Palamedes, is an extensible library for the Lean theorem prover. The synthesis algorithm itself is built on standard proof-search tactics, reducing implementation burden and allowing the algorithm to benefit from further advances in Lean proof automation.