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.

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.

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

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

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.

See Search.v for an example of search.

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.

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.

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.

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.

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.

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.

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!

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

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.

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

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.

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.

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.

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.

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.

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. 

This functionality is demonstrated in Example.v.

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.

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.

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.

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.

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.

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

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

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

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.

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.

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

• The Equivalences for Free! univalent parametricity framework (hereon EFF)
• Datamash

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.

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.

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).

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.

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.

• LICENSE: License
• plugin: Main directory for the plugin
  • build.sh: Build script
  • test.sh: Test script
  • coq: Tests and paper examples
    • examples: Paper examples (see paper examples section of this document for details)
    • playground: Preliminary thoughts on useful theory for later extensions to PUMPKIN Pi
    • Indtype.v: Lifting tests for inductive relations
    • Infrastructure.v: Testing infrastructure
    • ShouldFail.v: Tests that should currently fail
    • Test.v: Tests for search for algebraic ornaments
    • TestLift.v: Tests for lifting across algebraic ornaments
    • TestUnpack.v: Tests for unpacking indexed types
    • minimal_records.v: Basic tests for products and records
    • more_records.v: More advanced tests for products and records
    • NoSmartCache.v: Disabling the smart cache
    • SmartCache.v: Keeping the smart cache enabled
    • prod_rect.v: Test functionality that produces prettier terms
  • eval: Case study code and dependencies
    • equiv4free: EFF case study code and depedencies
      • Makefile
      • cast.v
      • lemmas.v
      • list.v
      • main.v: Main EFF case study code
      • perm.v
      • prepermutes.sh: Script to normalize pre_permutes
    • Makefile
    • cast.v
    • lemmas.v
    • main.v: Main ITP 2019 case study code
    • times.sed: Script to format times
    • together.sh: Main case study script
  • deps: Depedencies
    • fix-to-elim: Preprocessing with the fix-to-elim plugin
  • src: Source directory
    • coq-plugin-lib: Coq plugin library
    • lib: Internal library
    • automation: Automation directory
      • search: Search
      • lift: Lifting
      • unpack.ml and unpack.mli: Converting the unpacking tactic to a command
      • depelim.ml and depelim.mli: Automation for non-primitive projections
    • cache: Caching ornaments and lifted terms
      • caching.ml and caching.mli
    • components: Components in the style of PUMPKIN PATCH
      • abstraction.ml and abstraction.mli:
      • differencing.ml and differencing.mli:
      • factoring.ml and factoring.mli:
      • specialization.ml and specialization.mli:
    • ornaments: Internal representations and configuration
    • frontend.ml and frontend.mli: Main functionality for commands
    • options.ml and options.mli: Definitions of and access to options
    • ornamental.ml4: Top-level source file
    • ornaments.mlpack
  • theories: PUMPKIN Pi theories
    • Adjoint.v: Turning equivalences into adjoint equivalences
    • Prod.v: Preprocessed projections of pairs
    • Eliminators.v: Generalized smart eliminators for user-friendly types
    • Ornaments.v: Loader theory for PUMPKIN Pi
    • Unpack.v: Unpacking terms (Ltac tactic)
• .gitignore
• README.md

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.

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.