The Search for Constrained Random Generators

TL;DR

The paper tackles the problem of efficient constrained random generation in property-based testing by proposing a deductive synthesis framework that constructs correct-by-construction generators from predicates. Using a denotational semantics for generators and recursion schemes, Palamedes synthesizes generators in Lean via a rule-based proof search that yields executable, assume-aware generators with soundness and completeness guarantees. Key contributions include a formal Gen α representation, a suite of synthesis rules (e.g., $S$-Pure, $S$-Pick, $S$-Bind, $S$-List-Unfold), a recursion-scheme–driven approach for recursive predicates, and an implemented Lean library with evaluation on 32 benchmarks against Cobb and QuickChick. The work demonstrates that correct-by-construction generators can be generated offline, offering substantial speedups and broader applicability for inductive data types and well-typed programs, with practical impact for automating test generation. Future work targets sizing, broader predicate support, and cross-language backends to broaden real-world adoption.

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.

Figures (19)

• Figure 1: A recursive Lean predicate that checks if a tree is a BST.
• Figure 2: A handwritten generator for binary search trees.
• Figure 3: Synthesis rules for ${\color{cb-blue} \mathsf{pure}}$ and ${\color{cb-blue} \mathsf{pick}}$.
• Figure 4: Synthesis rule for ${\color{cb-blue} \mathsf{bind}}$ ($\ {\color{cb-blue} \mathbin{>{\mkern-10mu}>{\mkern-10mu}=}\ }$).
• Figure 5: Left: a version of using . Right: a version of using .

Theorems & Definitions (9)

• Definition 3.1
• Definition 3.2: Correctness
• Definition 3.3: Assume-Freedom
• Lemma 3.1: Choose Support
• Lemma 3.2: Elements Support and Synthesis
• Lemma 3.3: Optimizations Correct
• Lemma 4.1: Fold-Unfold-Inverse for Lists
• Lemma B.1: Greater Than Support
• Lemma B.2: Less Than Support