hs-to-rocq

Join our discussion on:

This repository contains a converter from Haskell code to equivalent Coq code, as part of the CoreSpec component of the DeepSpec project.

CPP'18 paper "Total Haskell is Reasonable Coq" by Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich. This paper describes the following examples:

• bag Multiset implementation from GHC's implemention
• compiler Hutton's razor
• base-src The sources of the base/ directory

ICFP'18 paper "Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report)" by Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, and Stephanie Weirich. This paper describes the verification of the containers library.

See paper-claims-audit.md for a detailed audit of which paper claims still hold on the current codebase (GHC 9.10.3, Coq 8.20, containers v0.7).

Documentation for the hs-to-rocq tool is available!

Installation

Current target: GHC 9.10.3 and Coq 8.20

Compilation

The recommended way of building hs-to-rocq is to use stack. If you have not setup stack before, run:

stack setup

To build hs-to-rocq, then run

stack build

Building the base library

This repository comes with a version of (parts of the) Haskell base library converted to Coq, which you will likely need if you want to verify Haskell code.

You must have Coq 8.20 and MathComp (with Hierarchy Builder) to build the base library and containers proofs. To install these tools:

1. opam repo add coq-released https://coq.inria.fr/opam/released (for SSReflect and MathComp)
2. opam update
3. opam install coq.8.20.1 coq-mathcomp-ssreflect coq-hierarchy-builder

Once installed, you can build the base library with

cd base && coq_makefile -f _CoqProject -o Makefile && make -j && cd ..

The directory base-thy/ contains auxiliary definitions and lemmas, such as lawful type-class instances. You can build these with

cd base-thy && coq_makefile -f _CoqProject -o Makefile && make -j && cd ..

Regenerating the base library

The base/ directory contains a convenience copy of the generated Coq files. To regenerate from Haskell source (requires the ghc-internal submodule):

git submodule update --init --recursive
make -C examples/base-src clean
make -C examples/base-src

This runs hs-to-rocq on the GHC 9.10 base/ghc-internal sources and compiles the resulting Coq files. Set LANG=C.utf8 if you encounter encoding errors (generated files contain Unicode characters like ∘).

Using the tool

To use the tool, run it (using stack), passing the Haskell file to be translated and an output directory to write to:

stack exec hs-to-rocq -- -o output-directory/ Input/File.hs

Very likely you want to make use of the base/ library. In that case, make sure you pass -e base/edits.

Have a look at the example directories, e.g. examples/successors, for a convenient Makefile based setup.

Edits

The edits file contains directives to hs-to-rocq for ignoring or transforming some Haskell constructs into proper Coq.

For example, it is common in Haskell to have the following code:

module Foo where
...
newtype SomeType = SomeType { someFiled :: Integer }

Coq has a single namespace for types and values hence the type name will conflict with constructor name. One can pass -e edit file containing custom directives to ensure correctness of generated code with the following directive:

rename value Foo.SomeType = Foo.MkSomeType

See the manual for documentation for the edits files.

Examples Status

All examples target Coq 8.20 and GHC 9.10.3. The table below shows the build status of every example directory.

Dependency Chain

base → base-thy → containers/lib → containers/theories
                 → transformers/lib
                 → ghc/lib → ghc/theories
                           → core-semantics/lib
                 → graph/lib → graph/theories (needs coq-equations)
                 → wc/lib (needs coq-itree)
                 → shuffle/lib (depends on transformers)
                 → compiler, rle, quicksort, dlist, coinduction,
                   intervals, successors, lambda, simple

Build Status

Build Commands

# Build everything that works
make                                    # base + base-thy + containers + ghc

# Individual examples (generate + compile)
make -C examples/compiler
make -C examples/dlist
make -C examples/rle
make -C examples/quicksort
make -C examples/coinduction
make -C examples/intervals
make -C examples/successors
make -C examples/lambda
make -C examples/simple

# Graph (lib compiles, theories needs coq-equations for 3 proof files)
cd examples/graph/lib && coq_makefile -f _CoqProject -o Makefile && make -j
cd examples/graph/theories && coq_makefile -f _CoqProject -o Makefile && make -j

# Transformers
cd examples/transformers && make

# Tests
make -C examples/tests
make -C examples/base-tests

Some examples use git submodules, so run

  git submodule update --init --recursive

once.

• structural-isomorphism-plugin: (In progress.) A GHC plugin that connects the re-extracted converted code back into GHC, allowing us to run Haskell programs against verified/verifiable code. Currently does not work.