ghc-proofs: GHC plugin to prove program equations by simplification

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain]

Warnings:

Often when writing Haskel code, one would like to prove things about the code.

A good example is writing an Applicative or Monad instance: there are equation that should hold, and checking them manually is tedious.

Wouldn’t it be nice if the compiler could check them for us? With this plugin, he can! (At least in certain simple cases – for everything else, you have to use a more dedicated solution.)

See the documentation in GHC.Proof or the project webpage for more examples and more information.


[Skip to ReadMe]

Properties

Versions0.1, 0.1, 0.1.1
Change logChangeLog.md
Dependenciesbase (>=4.9 && <4.11), ghc (>=8.2 && <8.4) [details]
LicenseMIT
Copyright2017 Joachim Breitner
AuthorJoachim Breitner
Maintainermail@joachim-breitner.de
CategoryCompiler Plugin, Formal Methods
Home pagehttps://github.com/nomeata/ghc-proofs
Source repositoryhead: git clone git://github.com/nomeata/ghc-proofs.git
UploadedSat Aug 26 09:16:10 UTC 2017 by JoachimBreitner

Modules

Downloads

Maintainers' corner

For package maintainers and hackage trustees


Readme for ghc-proofs-0.1

[back to package description]

Prove program equations with GHC

This GHC plugin allows you to embed code equation into your code, and have them checked by GHC.

Synopsis

See the GHC.Proof module for the documentation, but there really isn't much more to it than:

{-# OPTIONS_GHC -O -fplugin GHC.Proof.Plugin #-}
module Simple where

import GHC.Proof
import Data.Maybe

my_proof1 = (\f x -> isNothing (fmap f x))
        === (\f x -> isNothing x)

If you compile this, you will reassurringly read:

$ ghc Simple.hs
[1 of 1] Compiling Simple           ( Simple.hs, Simple.o )
GHC.Proof: Proving my_proof1 …
GHC.Proof proved 1 equalities

See the examples/ directory for more examples of working proofs (with GHC HEAD).

If you have proof that GHC cannot prove, for example

not_a_proof = (2+2::Int) === (5::Int)

then the compiler will tell you so, and abort the compilation:

$ ghc Simple.hs
[1 of 1] Compiling Simple           ( Simple.hs, Simple.o )
GHC.Proof: Proving not_a_proof …
Proof failed
    Simplified LHS: GHC.Types.I# 4#
    Simplified RHS: GHC.Types.I# 5#
    Differences:
    • 4# /= 5#

Simple.hs: error: GHC.Proof could not prove all equalities

How does it work?

GHC is a mighty optimizing compiler, and the centerpiece of optimizing, the simplifier is capable of quite a bit of symbolic execution. We can use this to prove program equalities, simply by taking two expressions, letting GHC simplify them as far as possible. If the resulting expressions are the same, then the original expressions are – as far as the compiler is concerned – identicial.

The GHC simplifier works on the level of the intermediate language GHC Core, and failed proofs will be reported as such.

The gory details are as follows: The simplifier is run 8 times, twice for each of the simplifier phases 4, 3, 2 and 1. In between, the occurrence analiser is run. Near the end, we also run common-subexpression elimination.

The simplifier is run with more aggressive flags. In particular, it is instructed to inline functions aggressively and without worrying about code size.

Why is this so great?

Why is this not so great?

What can it prove?

Not everything. By far.

But some nice, practical results work, see for example the proofs of the Applicative and Monad laws for Control.Applicative.Succs.

Best results were observed with compositions of non-recursive functions that handle non-recursive data or handle lists usind standard list combinators.

The GHC simplifier generally refuses to inline recursive functions, so there is not much we can do with these for now.

My proof is not found. What can I do?

The plugin searches for top-level bindings of the form

somename = proof expression1 expression2

or

somename = expression1 === expression2

GHC will drop them before the plugin sees them, though, if somename is not exported, so make sure it is exported. If you really do not want to export it, then you can keep it alive using the trick of

{-# RULES "keep somename alive" id somename = somename #-}

If it still does not work, check the output of -dverbose-core2core for why your binding does not have the expected form. Maybe you can fix it somehow.

My proof does not go through. Can I fix that?

Maybe. Here are some tricks that sometimes help:

Shall I use this in production?

You can try. It certainly does not hurt, and proofs that go through are fine. It might not prove enough to be really useful.

What next?

It remains to be seen how useful this approach really is, and what can be done to make it more useful. So we need to start proving some things.

Here are some aspects that likely need to be improved:

How else can I prove things about Haskell?

Can I comment or help?

Sure! We can use the GitHub issue tracker for discussions, and obviously contributions are welcome.