The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

Note that there has already been work on verifying LLVM passes using a
variant of your approach M2:

  Vellmv: Verifying the LLVM
  Steve Zdancewic, Dmitri Garbuzov, William Mansky, Vivien Durey, Milo
M. K. Martin, Jianzhou Zhao, Santosh Nagarakatte
  2012-2015
  http://www.cis.upenn.edu/~stevez/vellvm/

This project does not try to generate C++ code, it instead compiles
and run the OCaml program extracted from Coq. I think this is a
reasonable approach (using either inter-process communication of
textual or binary IR representations, or even directly OCaml bindings
to the LLVM machinery).

Another interesting project in this space is CompcertSSA:

  Gilles Barthe, Delphine Demange, David Pichardie, Léo Stefanesco
  2012-2015
  http://compcertssa.gforge.inria.fr/

It focuses more on interfacing with Compcert than LLVM (the SSA format
is designed from scratch with Coq proofs in mind, and thus is not LLVM
IR, although bidirectional conversions should be doable).

If you are interested in "interaction with the mainstream world", you
should also have a look at the Jitk project, which uses Compcert to
implement verified jitted interpreters for two in-Linux-kernel
interpreted languages, BPF and INET-DIAG.

  Jitk: A Trustworthy In-Kernel Interpreter Infrastructure
  Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, Zachary Tatlock
  2014
  https://people.csail.mit.edu/nickolai/papers/wang-jitk.pdf

On Tue, Jan 5, 2016 at 11:06 AM, Chan Ngo 
<chan.ngo2203 AT gmail.com>
 wrote:
> Dear all,
>
> Thanks for the references. The Herms’ thesis is exactly what I wanted to
> point out in the previous emails.
>
> This thread becomes interesting as on my side :-) By the way, I would like
> to turn the subject a little bit but in the same track. We consider the LLVM
> compiler, I assume that its core implementation is formally proved (e.g.,
> some work based on translation validation for proving the correctness of the
> compiler’s transformations and optimizations). Now, assume that I want to
> develop a new “pass” (an optimization - in C++ and uses the data structures
> and API functions provided by LLVM) for  LLVM and I want to make sure that
> my pass implementation is formally proved. I end up with two methods below:
>
> M1.
> - Develop a translation module that translates my code in C++ to Gallina (I
> think it is not easy task)
> - Prove the correctness of this module
> - Prove the correctness of the pass implementation based on the translated
> Gallina in Coq (i.e., based on the tool like VST)
>
> M2.
> - Specify the pass implementation in Coq, meaning that somehow we define a
> programming language with constructors coming from the data structures and
> API functions in LLVM (i.e., the concept of Basic Block, Functions, Modules
> in LLVM IR)
> - Prove the correctness of the pass based on the above specification in Coq
> (i.e., based on the tool like VST)
> - Automatically generated the C++ code of the pass from Coq
>
> How do you think about pros and cons of each methods?
>
> Thanks,
>
> ---
> Chan Ngo
> INRIA,
> (+33)02 99 84 72 84
> chan.ngo AT inria.fr
> http://people.rennes.inria.fr/Chan.Ngo