/pumpkin-pi

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.

Primary LanguageCoqMIT LicenseMIT

Coming here from the latest PLDI 2021 draft? The documentation below is meant for users and is a bit out of date. The PLDI 2021 draft code guide can be found here.

This is PUMPKIN Pi (formerly DEVOID), a plugin for automatic discovery of and lifting across equivalences between types in Coq. PUMPKIN Pi is a part of the PUMPKIN PATCH proof repair plugin suite, and is included as a dependency of PUMPKIN PATCH starting with release 0.1.

PUMPKIN Pi began as DEVOID, the artifact for the ITP paper Ornaments for Proof Reuse in Coq. It has since been extended. A version of PUMPKIN Pi that corresponds to the ITP camera-ready can be found in this release. A pre-print of our PLDI 2021 paper here.

Given two types A and B that are related in certain ways, PUMPKIN Pi can search for and prove the relation between those types, then lift functions and proofs between them. The following relations are currently supported automatically:

  1. Algebraic Ornaments: the type B (like vector) is the type A (like list) indexed by a fold over A (like length)
  2. Records and Tuples: the type A is a nested tuple of the form x * (y * ...), and the type B is a record with the same number of fields that have the same types
  3. Swapping and Renaming Constructors: the types A and B are two inductive types that are equal up to swapping constructor order and renaming constructors
  4. Escaping Sigma Types: the type B (like vector T n) is the type A (like { s : sigT (vector T) & projT1 s = n}) escaping the sigma type

It then ports functions and proofs across those equivalences. For changes that don't fall into the above four buckets, you need to supply the equivalence yourself in a deconstructed form called a configuration. If you need help with this, please check out two examples: switching between unary and binary natural numbers here, and an easier refactoring of constructors here. Also check out the PLDI 2021 draft here.

Getting Started

This section of the README is a getting started guide for users. Please report any issues you encounter to GitHub issues, and please feel free to reach out with questions.

Building PUMPKIN Pi

The only dependency you need to install yourself is Coq 8.9.1. PUMPKIN Pi also depends on a Coq plugin library which is included as a submodule automatically in the build script, and on the fix-to-elim plugin, which is also included. To build PUMPKIN Pi, run these commands:

cd plugin
./build.sh

Using PUMPKIN Pi

For an overview of how to use the tool, see Example.v and minimal_records.v.

Overview

At a high level, there are two main commands: Find ornament to search for equivalences (misleadingly named as an artifact of history and time constraints), and Lift (or Repair for tactic support) to lift along those equivalences. Find ornament supports two additional options to increase user confidence and to make the functions that it generates more useful. If you skip running the Find ornament command and just run Lift or Repair, then PUMPKIN Pi will run Find ornament for you automatically first.

In addition, there are a few commands that help make PUMPKIN Pi more useful: Preprocess for pattern matching and fixpoint support, and Unpack to help recover more user-friendly types. The Preprocess command comes from our plugin fix-to-elim.

Search

See Search.v for an example of search.

Command
Find ornament A B as A_to_B.

This command searches for the equivalence that describes the change from A to B, when the change is supported by automatic configuration.

Outputs

For algebraic ornaments, Find ornament returns three functions if successful:

  1. A_to_B,
  2. A_to_B_inv, and
  3. A_to_B_index.

A_to_B and A_to_B_inv form a specific equivalence, with A_to_B_index describing the fold over A.

For other kinds of equivalences, Find ornament returns only the first two of these.

Options for Correctness

Find ornament supports two options. By default, these options are disabled. Together, setting these two options tells Find ornament to prove that its outputs are correct. (Also as an artifact of time constraints, the options use the old name, DEVOID.)

Set DEVOID search prove coherence.

For algebraic ornaments, this option tells Find ornament to additionally generate a proof A_to_B_coh that shows that A_to_B_index computes the left projection of applying A_to_B.

Set DEVOID search prove equivalence.

This option tells Find ornament to generate proofs A_to_B_section and A_to_B_retraction that prove that A_to_B and A_to_B_inv form an equivalence.

Using Custom Equivalences with Automatic Configuration

If Find ornament fails for an automatic configuration or you would like to use an existing equivalence, you can run this command before lifting (still misleadingly named as an artifact of history and time constraints):

Save ornament A B { promote = f; forget = g}.

where f and g form an equivalence that describes one of the supported relations between A and B. Note that support for this is extremely experimental, and will not yet work if you try this with changes not supported by automatic configuration (you will need manual configuration for that; more below). You can find an example in TestLift.v.

You can also use this to substitute in a different equivalence for an existing equivalence, but again there are some restrictions here on what is possible. See ListToVectCustom.v for more information.

You can also skip one of promote or forget, provide just one, and let PUMPKIN Pi find the other for certain automatic configurations, for example:

Save ornament A B { promote = f }.

This is especially useful when there are many possible equivalences and you'd like to use a particular one, but let PUMPKIN Pi figure out the rest. See Swap.v for examples of this.

Using Custom Equivalences with Manual Configuration

To use a custom equivalence not at all supported by one of the four search procedures, like switching between unary and binary natural numbers, check out two examples here and here. These examples set manual configuration and essentially skip the search procedure. We will document them soon! The arXiv paper says a lot about these but the examples are the best place to look for now.

Ambiguity

Sometimes, automatic configuration of PUMPKIN Pi finds multiple possible equivalences. With swapping constructors in particular, there can be an exponential number of possible equivalences.

In the case of ambiguity, PUMPKIN Pi presents up to the first 50 possible options for the user (in a smart order), presents this as an error, and gives instructions for the user to provide more information to Find ornament in the next iteration. If the equivalence you want is not in the first 50 candidates, please use Save ornament. See Swap.v for examples of both of these.

Tactic Support

PUMPKIN Pi produces tactic suggestions for all proofs that Find ornament finds. These are experimental, especially with dependent types, but may help you work with tactic proofs about equivalences. You should think of these as suggestions to tweak. Improving the decompiler to both be sound and produce intuitive tactics that match common proof engineering styles is an ongoing project!

Lift and Repair

See Example.v, minimal_records.v, and Swap.v for examples of lifting.

Command
Lift A B in f as g. (* no tactic suggestions *)
Repair A B in f as g. (* tactic suggestions *)

This command lifts a function or proof f along the configured equivalence. If you have already called Find ornament on A and B, it will use the discovered equivalence. If you have used manual configuration, it will use that configuration. Otherwise, it will search for an equivalence first.

Outputs

Lift or Repair produces a term g which is the analogue of f, but refers to B in place of A.

Alternate Syntax

You can run this with an alternate syntax as well:

Lift A B in f as ..suffix.
Repair A B in f as ..suffix.

This will name the result f_suffix.

Whole Module Lifting

You can lift an endure module across an ornament all at the same time by running this command:

Lift Module A B in Foo as Bar. (* no tactic suggestions *)
Repair Module A B in Foo as Bar. (* tactic suggestions *)

This will create a new module Bar with all of the liftings from Foo.

Tactic Support

Using Repair instead of Lift in thte above commands gives you tactic suggestions. These tactic suggestions are experimental, but may help you with workflow integration.

To suggest decision procedures to try to improve tactic output, you can pass the hint option, like:

Repair Module A B in Foo as Bar { hint : "ring" "auto" }

This option comes after opaque, like:

Repair Module A B in Foo as Bar { opaque : A_rect B_rect; hint : "ring" "auto" }

At some point, we hope to make it possible to reuse the tactics from the original proof script easily, even when they are not decision procedures.

Prettier Types

By default, PUMPKIN Pi lets Coq infer the types of lifted terms. You can instead tell PUMPKIN Pi to lift the types (these are typically prettier) if you set the following function:

Set DEVOID lift type.
Opaque Terms

If you'd like, you can tell the Lift or Repair command to treat certain terms as opaque when you are positive that lifting them will have no effect:

Lift A B in f as g { opaque constant1 constant2 ... }.
Repair A B in f as g  { opaque constant1 constant2 ... }.

This can make lifting much faster. It is strongly advisable to do this for certain terms that you know PUMPKIN Pi should never reduce. However, this can also cause unpredictable errors if your assumption is incorrect, so be careful about your assumption.

You can also set a term to be globally opaque every time you lift between A and B by using the following command:

Configure Lift A B { opaque constant1 constant2 ... }.

You can find an example of this in more_records.v.

Caching

PUMPKIN Pi by default caches all lifted terms it encounters as it goes in order to save time. You can disable this if you'd like by running this command:

Unset DEVOID smart cache.

Additional Functionality

This functionality is demonstrated in Example.v.

Preprocess

The Lift command does not support pattern matching and fixpoints directly. To lift a function f' that uses pattern matching and (certain) fixpoints, run:

Preprocess f' as f.

Then, run:

Lift A B in f as g.

You can also run Preprocess on an entire module; see ListToVect.v for an example of this. See the fix-to-elim plugin for more functionality for Preprocess.

Bonus Features for Algebraic Ornaments

When lifting across algebraic ornaments, to recover a slightly more user-friendly type for a lifted term g with very little extra work, run:

Unpack g as g_u.

The type after Unpack still may not be very user-friendly. If you would like to put in a little more work to get back types that are very user friendly, check out the methodology in Example.v. The key is to set the following option:

Set DEVOID search smart eliminators.

This generates a useful induction principle. Using that induction princple and composing this by lifting across another equivalence, you can get from your unlifted type A to B at a particular index, with much nicer type signatures.

Assumptions for Automatic Configuration with Algebraic Ornaments

PUMPKIN Pi makes some assumptions about your terms and types for now (described in Section 3 of the ITP 2019 paper). Assumptions.v describes these assumptions in more detail and gives examples of unsupported terms and types. Note that the assumptions for records and tuples are not yet documented, since support for those types is brand new.

These assumptions are mostly to simplify search. We hope to loosen them eventually. If any are an immediate inconvenience to you, then please cut a GitHub issue with an example you would like to see supported so that we can prioritize accordingly.

Known Issues

Please see our GitHub issues before reporting a bug (though please do report any bugs not listed there).

One outstanding issue (an unimplemented optimization) has consequences for how we lift and unpack large constants compositionally. For now, for large constants, you should prefer lifting several times and then unpacking the result several times over iteratively lifting and unpacking. See this issue.

There are also still some open questions about eta expansion and definitional equality. Practically, from a user's perspective, that means that lifting may sometimes fail with mysterious type errors for types that look almost but not quite correct. Rest assured, we are working on fixing this, or at the least understanding why it happens well enough to significantly improve error messaging and rule out invalid inputs.

Examples

This part of the README explains some examples and how they correspond to the ITP 2019 paper. You may find these useful as a user, as a reader, or as a developer.

ITP 2019 Paper Examples

The example from the paper are in the examples directory. Here is an overview of the examples, in order of relevance to the paper:

  • Intro.v: Examples from Section 1 of the paper
  • Example.v: Motivating example from Section 2 of the paper
  • Assumptions.v: Assumptions from Section 3 of the paper
  • LiftSpec.v: Intuition for lifting from Section 3 of the paper
  • Search.v: Search examples from Section 4 of the paper
  • Lift.v: Lifting examples from Section 4 of the paper
  • ListToVect.v: Example of preprocessing a module from Section 5 of the paper
  • Projections.v: Evidence for non-primitive projection claims from Section 5 of the paper

Tuple and Record Examples

The most useful examples of lifting between tuples and records are in minimal_records.v and more_records.v.

Swapping and Renaming Constructors Examples

The most useful examples of swapping and renaming constructors are in Swap.v.

Other Examples

The coq directory has more examples, including regression tests and examples from the arXiv paper.

The eval directory has examples from the case study from Section 6 of the ITP 2019 paper. They may be a bit hard to read since there is some scripting going on. They may still be interesting to you whether or not you want to actually run the case study.

ITP 2019 Case Study

This section of the README describes how to reproduce the case study from Section 4 of the ITP 2019 paper. The case study is in the eval directory. We support the case study scripts on only Linux right now.

Building the Case Study Code

To run the case study code, you need the following additional dependencies:

Run the following to make EFF:

cd <path-to-EFF>
make && make install

Datamash should install in a straightforward way from a package manager using the link above.

Reproducing the Paper Case Study

The particular commit for EFF used for the results in the paper is this commit. We have rerun the experiments using this commit, the newest commit at the time of release, and there results have not changed significantly. Results are not guaranteed to be the same for different commits of EFF, especially later ones which may include optimizations not yet implemented at the time of writing. Similarly, on different architectures, the numbers may be slightly different; the orders of magnitude should be comparable.

Enter the eval directory:

cd eval

Increase your stack size:

ulimit -s 100000

Run the following script:

./together.sh

The script takes a while, as it runs each function ten times each on large data both for PUMPKIN Pi and for EFF. When it is done, check the results folder for the median runtimes as well as the size of reduced functions. This also does a sanity check to make sure both versions of the code produce the same output. It does not yet try to reduce the proof of pre_permutes using EFF, otherwise the case study would take a very long time to run. To run this just once, enter the equiv4free directory:

cd equiv4free

In that directory, uncomment the following line in main.v:

(*Redirect "../out/normalized/pre_permutes-sizedEFFequiv" Eval compute in pre_permutes'.*)

Then run the following script, which runs the EFF code just once:

./prepermutes.sh

This should take a while (how long depends on your architecture) and produce a very large term.

Understanding the Case Study Code

The code for the case study is in the eval folder. The case study uses the same exact input datatypes for both PUMPKIN Pi and EFF, copying and pasting in the inputs, lifted functions, and equivalences PUMPKIN Pi produces to run on the dependencies of EFF. The reasons for copying the inputs are that EFF has different Coq dependencies, so the base functions perform differently. In addition, lifting constants with EFF additionally slows down performance, and we would like to control for only the performance of lifted functions, which is easiest to understand.

There is one other thing worth understanding about the case study code. We used to use this command to measure the performance of foo:

Eval vm_compute in foo.

An ITP reviewer noted that this includes the amount of time to print foo. This is a lot of overhead that clouds the usefulness of the data. The reviewer suggested writing:

Eval vm_compute in (let _ := foo in tt).

Unfortunately, Coq seems to be a bit too smart for that; it doesn't actually bother computing foo if you do that. Instead, we now write:

Eval vm_compute in (List.tl [foo]).

This forces Coq to compute foo, but ultimately prints [], thereby not adding printing time. It does add the time to run List.tl, but this overhead is very minimal on a list of a single element (much more minimal than the overhead of printing).

Implementation and Development

Transparency is very important to me and my coauthors. My goal is not just to produce a useful a tool, but also to demonstrate ideas that other people can use in their tools.

Some information for transparency is in the paper: Section 4 discusses the core algorithms that PUMPKIN Pi implements, and section 5 discusses a sample of implementation challenges.

This part of the README is here to complement that. It describes the structure of the code a bit. It should also help if you are interested in contributing to PUMPKIN Pi, or if you are interested in using some of the libraries from PUMPKIN Pi in your code.

Understanding the Code

This is an outline of the structure of the code. Please cut an issue if you are confused about anything here. Please also feel free to ask if you are confused about anything that the code does.

Regression Testing

The test script in the plugin directory runs all of the regression tests:

./test.sh

After making a change to PUMPKIN Pi, you should always run this. You should also run the case study scripts to check performance.

Licensing and Attribution

PUMPKIN Pi is MIT licensed, since I have a very strong preference for the MIT license and since I believe I do not need to use Coq's LGPL when writing language plugins. This interpretation might be wrong, though, so I suppose you should tread lightly. If you are an expert in licensing, definitely let me know if this is wrong.

Regardless, I would like PUMPKIN Pi to be used freely by anyone for any purpose. All I ask for is attribution, especially in any papers that you publish that use PUMPKIN Pi or any of its code. Please cite the ITP paper or the arXiv paper when referring to PUMPKIN Pi in those papers.