Random generators for Strata Core programs

This repo contains random generators for well-typed Strata Core programs. These generators are built using the Basalt Lean framework, which allows us to prove these generators sound and complete with respect to Strata Core's typing relations.

Specifically, the repo contains generators for the following fragment of Strata Core:

• Expressions (LExprs) (typing relation: HasTypeA)
  • Note: our LExpr generator targets the HasTypeA typing relation (which pertains to well-annotated locally nameless terms), not HasTypeA
• Commands (typing relation: CmdHasTypeA)
• Functions (typing relation: FunctionHasTypeA)
• Statements & statement sequences (typing relation: StmtHasTypeA, StmtsHasTypeA)
• Procedures (typing relation: ProcHasTypeA)
• Whole programs (typing relation: ProgramHasTypeA)

Generator Interpretations

Basalt generators are polymorphic in their monad (see the Basalt repo for more details): this means they can be interpreted differently for execution / proofs.

• To run these generators, we interpret them using Plausible's Gen monad.
• To prove properties about the generators, we interpret them using SetGen, which reasons about a generator's support (the set of all values that can be produced by the generator)

Note: Basalt allows reasoning about generators' distributions via another interpretation (SPMF, in which generators are viewed as sub-probability mass functions), but this repo does not use this interpretation at the moment. SetGen.lean contains SetGen variants of some SPMF results that appear in the Basalt source code, which are required for proofs about Strata generators.

Organization

Each generator is split into a Core.lean (containing the generator's executable code) and a separate proof file. For example, for the LExpr generator, HasTypeAGen/Core.lean contains the actual code for the generator, while HasTypeAGen.lean contains the generator's correctness proofs. This allows us to avoid importing both Strata and Batteries (imported transitively via Mathlib) in the same file, as List.Forall₂ is defined by both libraries.

Dependencies

• Strata
• Basalt (used for proving generators correct)
• Plausible (used to run generators)
• LSpec (Lean testing framework, we use LSpec's test harnesses to run tests)
• (Optionally) An SMT solver (cvc5 or z3) to test Strata properties related to SMT encoding, which are not run by default
  • See the installation instructions in the Strata repository on how to install cvc5/z3

Building

1. Resolve dependencies and fetch prebuilt artifacts:

   lake update
   lake exe cache get

2. Build:

   lake build

3. Run a small amount of tests (note the --quick flag, which runs each property with 100 random inputs):

   lake test -- --quick
   

Running tests using these generators

To run a test executable, which tests a variety of properties using these Strata Core generators, run lake test -- --quick. (The --quick flag minimizes the no. of tests run, if we omit this flag, the entire test suite, consisting of 80+ properites, takes 10+ minutes to run. This is because it runs each property with 1000 random trials, with the randomly generated inputs having a larger size.)

This executable runs a Plausible test suite via LSpec, and visualizes test results using Tyche, a VS Code extension for inspecting property-based testing generators.

If you want to manually configure the no. of trials / size of inputs, you can pass them through to the test driver after --:

lake test -- [numTrials] [maxSize] [flags]

Alternatively, you can also build & run the test executable directly as follows:

lake build test
.lake/build/bin/test [numTrials] [maxSize] [flags]

• numTrials (default: 1000) —: umber of random test cases per property
• maxSize (default: 5): maximum size parameter for generation (controls the depth of the generated AST)

Flags (all optional; the Tyche visualization pass is on by default):

• --quick runs a small no. of tests with a small size, prioritizing fast results. Currently, this flag runs 100 trials for each property, with size = 2 passed to the generators. This flag omits Tyche visualizations:
• --no-tyche: omit Tyche visualizations (i.e. only run tests)
• --tyche-out=PATH: output filepath for JSON files storing test metadata which is ingested by Tyche (this defaults to tyche_output.jsonl)
• --tyche-samples=N — no. of test samples visualized per Tyche panel (default 1000)
• --smt — Tests properties related to Strata SMT encodings. This CLI flag requires a local installation of an SMT solver (cvc5/z3). If --smt is passed but the SMT solver cannot be run, the test harness emits an error and exits with a non-zero exit code.

See properties_bugs_found.md for the full list of properties tested & bugs found. For the actual code for the properties, refer to the StrataTests/ directory (see the Adding a new property section below for more details on how this directory is organized).

LSpec-free harness (test-plain)

There is a second test executable, test-plain, that does not depend on LSpec. All properties, generators and CLI flags are shared with the default test runner (the one inovked by doing lake test).

To run the alternate test-plain harness, do:

lake build test-plain
.lake/build/bin/test-plain [numTrials] [maxSize] [--smt]

test-plain keeps the LSpec dependency droppable. LSpec reaches this package only through a fork that is pinned to Lean 4.29, because mainline LSpec is on Lean 4.31.

Tuning the generators' distributions

A generator's distribution is controlled by a set of weights called a tuning (these are the Nat weights which are passed to Basalt's frequency combinator, which chooses between a list of sub-generators based on the weights provided).

We have observed that effective testing of different properties necessitates different generator distributions. For example, for testing loop-related Strata Core transformations, we want to tune our generators so that they generate programs containing loops more frequently.

To target different testing scenarios, we have come up with different sets of generator weights (obtained empirically) which increase the frequency of generating programs that exercise different Strata Core language features.

These are stored in TuningProfiles.lean and ProgramTuning.lean: here is a full list of the weights:

Lean file	Tunings
TuningProfiles.lean	stmtLoopHeavy (prioritizes loops) stmtFuncDeclHeavy (prioritizes function declarations) stmtLoopWide (prioritizes non-nested loops) stmtMixed (general-purpose distribution for statements that exercises loop-related transformations & as well as the detToKleene pass) procCallHeavy (prioritizes procedure call statements) procPrecondHeavy (prioritizes functions with preconditions) cmdSetHeavy (prioritizes the .set command) cmdInitHeavy (prioritizes the .init command) cmdCheckHeavy (prioritizes the .check command) exprEvalHeavy (prioritizes expressions that are not values, i.e. expressions that change under evaluation) exprQuantHeavy (prioritizes expressions with universal / existential quantification) exprIndirHeavy (prioritizes factory function calls) exprFVarHeavy (prioritizes expressions with free variables) tyCompoundHeavy (prioritzes compound types, such as functions, Map & Sequence)
ProgramTuning.lean	progPolyHeavy (prioritizes polymorphic functions) progDatatypeHeavy (prioritzes algebraic data type definitions)

Note: at time of writing, the generators for GenFunction, GenAdtBlock and GenIndepBlock do not support tuning.

(Aside: These weights were measured using the dist-report executable in this repo, which measures the frequency of different Strata Core language features in the generated programs. Run lake exe dist-report to see measurements, but note that end-users of this repo, e.g. Strata engineers, should not need to use this executable -- the pre-computed weights measured above should be sufficient.)

To override the default distribution used for a generator for a particular property, add the tuning argument to the strata_property and specify a named tuning, like so:

-- This overrides the generator to use a tuning which prioritizes generating loops, 
-- since we are testing a Strata Core transformation involving loops
@[strata_property (tuning := stmtLoopHeavy)] -- <- Note the `tuning` argument here!
def loopElimZeroLoops : TestDecl :=
  .property "stmt: LoopElim eliminates all loops"
    fun (gs : GenStmts) => checkLoopElimZeroLoops gs.stmts

Adding a new property

Properties to test are defined in the StrataTests/ directory. As an end-user of this library, you can add properites to either an existing file in StrataTests/, or create a new file in StrataTests/.

To add a new property (e.g. to test that a new pass myPass is idempotent), add the following:

import StrataGenerators.Test

open Core
open StrataGenerators.Test

-- This registers a new property
-- As the user, you can customize the name for the property in the string 
-- (Note that this name must be unique among all properties in the test suite)
@[strata_property]
def myPassIdempotent : TestDecl :=
  .property "mypass: the pass is idempotent"
    fun (gp : GenProgram) => myPass (myPass gp.prog) = myPass gp.prog

(For another example, see StrataTests/Example.lean.)

See "Choosing the input type" below for instructions on how to pick the right type to be generated. Note that the body of the function should be a Prop that is decidable (or alternatively a function that returns Bool). In our experience, functions that are decidable Props have better error messages (coming from the Plausible property-based testing library).

Note: properties that are Props should be defined using abbrev or be defined as @[reducible] def, in order for typeclass resolution to succeed.

The @[strata_property] attribute records the test declaration, allowing the test driver to pick it up.

If you added / removed a file in StrataTests/, run the following in order to populate the test executable (StrataTests.lean) with the appropriate import statements. Note that users should not modify StrataTests.lean by hand.

lake exe write-test-imports

Then, run the following:

# This lists all properties in the test suite, to confirm your new property was registered
lake test -- --list    

# Test only properties whose names begin with the substring "mypass:"
lake test -- --only="mypass:" --quick

# Test all properties (with only 100 inputs per property to minimize time spent)
lake test -- --quick

Choosing the input type

These are the types in the Strata Core AST for which we support random generation. Each type corresponds to a fragment of the Strata Core language.

All of these types already have instances of the Arbitrary, Repr, Shrinkable and TycheFeatures typeclasses, allowing them to be randomly generated, pretty-printed, shrunk (minimized when a counterexample to a property is found) and visualized using the Tyche VS code extension (see the Tyche visualization section below).

The function argument in the property should be one of the following types:

Type	Term produced by random generation
TypedExpr	a well-typed expression with its type, over defaultFCtx
ClosedTypedExpr	a well-typed closed expression (no free variables)
ResolveTypedExpr	a closed expression over coreOpCtx
GenCmdWithCtx / GenCmdsWithCtx	a command, or a command sequence, with its input & output contexts
GenFunction / ClosedGenFunction	a function (pure), with free variables coming from defaultFCtx or no free variables (closed function)
GenStmts	a well-typed sequence of statements
GenProcs	a list of well-typed procedures
GenProgram	an entire well-typed Strata Core program, including top-level declarations (Algebraic data type definitions, abstract types, type aliases, axioms)
GenAdtBlock / GenIndepBlock	a mutual … end datatype block containing (possibly mutually recursive) ADT definitions

If the Strata Core AST changes in the future and we gain new type definitions, to support these new types, users need to implement instances of the Arbitrary, Repr, Shrinkable, TycheFeatures typeclasses for it.

Defining families of properties

If multiple properties share the same input type (e.g. stating multiple properties about the LoopElim transformation over statements), we can define them using the @[strata_properties] attribute, like so:

-- Each property is an entry in a list passed to `family`, specifically 
-- a tuple consisting of the property name and the actual property function
@[strata_properties]
def stmtTransforms : List TestDecl :=
  family GenStmts
    [ ("stmt: LoopElim preserves typeability", fun gs => checkLoopElimPreservesTyping gs.stmts),
      ("stmt: LoopElim eliminates all loops",  fun gs => checkLoopElimZeroLoops gs.stmts) ]

Note the use of family macro, which allows us to define a list of properties (instead of defining properties one by one).

Marking individual properties as known to fail

If a property is known to fail, we can prefix the property using the knownFailure function and supply a string containing the failure reason, like so:

@[strata_property]
def myPassOutputTypechecks : TestDecl :=
  knownFailure "strata-org/Strata#123: the pass drops a type annotation on a nested call" <|
    TestDecl.property "mypass: the output typechecks"
      fun (gp : GenProgram) => checkMyPassOutputTypechecks gp.prog

The test suite then avoids reporting counterexamples that cause this property to fail, facilitating bug triage.

If the property is part of a family, we add .knownFailure "<failure_reason>" as an extra component of the tuple corresponding to the property. For example, using the stmtTransforms example above, if we wanted to mark the LoopElim eliminates all loops property as known to fail, we would do this:

def stmtTransforms' : List TestDecl :=
  family genStmts [
    ("stmt: LoopElim eliminates all loops",  fun gs => checkLoopElimZeroLoops gs.stmts, 
    .knownFailure "<failure_reason>"),
    ...
  ]

Tyche visualization

One can visualize the generators' output distributions with Tyche, a VS Code extension for inspecting property-based testing generators.

Generating samples

The boilerplate code to produce Tyche visualizations are automatically added when a new property is registered. By default, the test driver updates the Tyche panels in VS Code (the --quick / --no-tyche CLI flags suppress this behavior).

To add auxiliary information to a Tyche panel, modify the instance of the TycheFeatures typeclass for the type being generated (see StrataGenerators/Test/Generators.lean for details). For example, one can add a feature that explains why a property-based test failed (rejection_cause).

To further control the Tyche visualizations, use these CLI flags:

• --tyche-samples=N (default: 1000) — number of samples per generator
• --tyche-out=PATH (default: tyche_output.jsonl) — output file path

The Tyche visualizations dominate the runtime of the lake test executable. By default, the --quick CLI flag suppresses Tyche visualizations. To get the smaller no. of trials via the --quick flag while still having Tyche visualizations, pass the following CLI args manually to the test executable:

.lake/build/bin/test 100 40 --tyche-samples=200

Viewing Tyche visualizations

Open VS Code, press Cmd+Shift+P (on macOS), run Tyche: Open, and select the generated .jsonl file. Tyche displays interactive histograms and distribution charts for each property.

Checking that the Tyche visualizations appear

Run the following to produce the Tyche visualizations with a small no. of tests:

lake build test
.lake/build/bin/test 100 40 --tyche-samples=200

Then, in VS Code, do Cmd+Shift+P → Tyche: Open, and click on the relevant panel.

License

The contents of this repository are licensed under the terms of either the Apache-2.0 or MIT license, at your choice. See LICENSE-APACHE and LICENSE-MIT for details of the two licenses.