Skip to content

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

License

Notifications You must be signed in to change notification settings

uwplse/pumpkin-pi

Repository files navigation

This is DEVOID, a plugin for automatic discovery of and lifting across algebraic ornaments in Coq. It is the artifact for the ITP paper Ornaments for Proof Reuse in Coq. Please cite this paper when referring to DEVOID. A version of DEVOID that corresponds to the ITP camera-ready can be found in this release.

Basically, when you have two types A (like list) and B (like vector), where B is A indexed by some new type (like nat) that is determined by a fold over A (like length), DEVOID can search for the fold and functions that relate A and B, and then lift functions and proofs between types. The lifted functions and proofs are usually about as fast as the originals. See the paper and the examples for more detail.

DEVOID will eventually be a part of PUMPKIN PATCH. The top-level functionality will likely move into that repository. This repository will likely still contain some libraries and DEVOID-specific functionality. Please stay tuned.

Getting Started with DEVOID

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 DEVOID

The only dependency to use DEVOID is Coq 8.8. To build DEVOID, run these commands:

coq_makefile -f _CoqProject -o Makefile
make && make install

Using DEVOID

For a complete overview of how to use the tool, see Example.v. For those interested, more details can be found in Sections 2, 3, 4, and 5 of the paper.

Overview

At a high level, there are two main commands: Find ornament to search for ornaments, and Lift to lift along those ornaments. Find ornament supports two additional options to increase user confidence and to make the functions that it generates more useful.

In addition, there are two commands that help make DEVOID more useful: Preprocess for pattern matching and fixpoint support, and Unpack to help recover more user-friendly types. There is also work in progress on a general methodology (which will hopefully be automated in the future) to get even more user-friendly types.

Search

See Example.v for an example of search.

Command
Find ornament A B as A_to_B.

This command searches for the relation that describes the algebraic ornament between A and B.

Outputs

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.

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.

Set DEVOID search prove coherence.

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.

Lift

See Example.v for an example of lifting.

Command
`Lift A B in f as g.`

This command lifts a function or proof f along the discovered relation. You must call Find ornament on A and B before calling this command.

Outputs

Lift produces a function g which is the analogue of f.

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.

Unpack

To recover a slightly more user-friendly type for a lifted term g, run:

Unpack g as g_u.
User-Friendly Types

The type after Unpack still may not be very user-friendly. Example.v describes how to recover even more user-friendly types for lifted terms.

For the status of a general methodology for this, see GitHub issue #39.

Assumptions

DEVOID makes some assumptions about your terms and types for now (described in Section 3 of the paper). Assumptions.v describes these assumptions in more detail and gives examples of unsupported terms and types.

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.

Examples

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

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

Other Examples

The coq directory has more examples. These examples are regression tests, and so are not guaranteed to be useful to users. However, if you would like more examples, you may look there as well.

The eval directory has examples from the case study from Section 6 of the 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.

Case Study

This section of the README describes how to reproduce the case study from Section 4 of the 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 DEVOID 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 DEVOID and EFF, copying and pasting in the inputs, lifted functions, and equivalences DEVOID 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 DEVOID 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 DEVOID, or if you are interested in using some of the libraries from DEVOID 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 DEVOID, you should always run this. You should also run the case study scripts to check performance.

Licensing and Attribution

DEVOID 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 DEVOID to be used freely by anyone for any purpose. All I ask for is attribution, especially in any papers that you publish that use DEVOID or any of its code. Please cite the ITP paper when referring to DEVOID in those papers.