GitHub - ngernest/chamelean: Property-based testing for Lean via metaprogramming (original) (raw)

Chamelean is an extension of Lean's Plausible property-based testing library which automatically derives generators, enumerators and checkers for inductive relations.

Our design is heavily inspired by Coq/Rocq's QuickChick library and the following papers:

Overview

Like QuickChick, we provide the following typeclasses:

We provide various top-level commands which automatically derive generators for Lean inductives:

1. Deriving unconstrained generators/enumerators
An unconstrained generator produces random inhabitants of an algebraic data type, while an unconstrained enumerator enumerates (deterministically) these inhabitants.

Users can write deriving Arbitrary and/or deriving Enum after an inductive type definition, e.g..

inductive Foo where ... deriving Arbitrary, Eunm

Alternatively, users can also write deriving instance Arbitrary for T1, ..., Tn (or deriving instance Enum ...) as a top-level command to derive Arbitrary / Enum instances for types T1, ..., Tn simultaneously.

To sample from a derived unconstrained generator, users can simply call runArbitrary, specify the type for the desired generated values and provide some Nat to act as the generator's size parameter (10 in the example below):

#eval runArbitrary (α := Tree) 10

Similarly, to return the elements produced form a derived enumerator, users can call runEnum like so:

#eval runEnum (α := Tree) 10

2. Deriving constrained generators (for inductive relations)
A constrained producer only produces values that satisfy a user-specified inductive relation.

We provide two commands for deriving constrained generators/enumerators. For example, support we want to derive constrained producers of Trees satisfying some inductive relation balanced n t (height-n trees that are balanced. To do so, the user would write:

-- #derive_generator & #derive_enumerator derive constrained generators/enumerators -- for Trees that are balanced at some height n, -- where balanced n t is a user-defined inductive relation #derive_generator (fun (t : Tree) => balanced n t) #derive_enumerator (fun (t : Tree) => balanced n t)

To sample from the derived producer, users invoke runSizedGen / runSizedEnum & specify the right instance of the ArbitrarySizedSuchThat / EnumSizedSuchThat typeclass (along with some Nat to act as the generator size):

-- For generators: #eval runSizedGen (ArbitrarySizedSuchThat.arbitrarySizedST (fun t => balanced 5 t)) 10

-- For enumerators: -- (we recommend using a smaller Nat as the fuel for enumerators to avoid stack overflow) #eval runSizedEnum (EnumSizedSuchThat.enumSizedST (fun t => balanced 5 t)) 3

Some extra details about the grammar of the lambda-abstraction that is passed to #derive_generator / #derive_enumerator:

Specifically: in the command

#derive_generator (fun (x : t) => P x1 ... x .... xn)

P must be an inductively defined relation, x is the value to be generated (the type annotation on x is required), and x1 ... xn are (implicitly universally quantified) variable names. Following QuickChick, we expect x1, ..., xn to be variable names (we don't support literals in the position of the xi currently).

3. Deriving checkers (partial decision procedures) (for inductive relations)
A checker for an inductively-defined Prop is a Nat -> Option Bool function, which takes a Nat argument as fuel and returns none if it can't decide whether the Prop holds (e.g. it runs out of fuel), and otherwise returns some true/some false depending on whether the Prop holds.

We provide a command elaborator which elaborates the #derive_checker command:

-- #derive_checker derives a checker which determines whether Trees t -- satisfy the balanced inductive relation mentioned above #derive_checker (balanced n t)

Repo overview

Building & compiling:

Typeclass definitions:

Combinators for generators & enumerators:

Algorithm for deriving constrained producers & checkers (adapted from the QuickChick papers):

Derivers for unconstrained producers:

Miscellany:

Tests & Examples:

Tests

Overview of snapshot test corpus:

Key Value Store Example:

Cedar Example:

Tests for Unconstrained Generators (#derive_arbitrary):

Tests for Constrained Generators (#derive_generator):

Tests for Checkers (#derive_checker):

Tests for Unconstrained Enumerators (#derive_enum):

Tests for Constrained Enumerators (#derive_enumerator):

Enumerator Infrastructure Tests:

Auxiliary definitions for snapshot tests:

Plausible Tests (inherited from the original Plausible repo):