Compilation with a witness / certificate

Question

Sometimes, to install a program, you have a choice between compiling it yourself or downloading a precompiled binary. In theory (using a new programming language and a new compiler designed specifically for this), is it possible to generate a witness / certificate with the compiled binary such that checking the witness / certificate is very easy when compared to compiling things yourself, but ensures that the compilation indeed yields this binary ?

To avoid trivial answers, I'll specify things a bit more: The source language should contain ML, and the target language should be some realistic assembly language. The compiler should do many optimizations so that speed of the compiled program is comparable to that of OCaml, and in particular the compilation can not be just concatenating an interpreter and the source.

From what I've read, the longest thing in compilation is the optimizations. So my question is more or less: Can optimizations run much faster on a non-deterministic machine (in which case, we can use the witness to know which path to take on the real machine).

Answer 1

In theory, what you are asking about has been studied, under the name "translation validation". See, e.g., the following classic paper:

George C. Necula. "Translation validation for an optimizing compiler." PLDI 2000.

In practice, compilation is such a complicated messy process that I doubt there will be any easy-to-verify certificate that proves the entire compilation process was done correctly (including lexing, parsing, front-end, optimization, back-end, assembly, linking, etc.). Academic work typically focuses on just one or two phases of the process (e.g., some of the stages of optimization).

One should separate two separate issues: can the verifier be simpler than the compiler? can the verifier be faster than the compiler?

Simpler is interesting, because it means the verifier can potentially be more trustworthy (e.g., less likely to have bugs). Classic work on translation validation focuses on that case.

Faster is a different question. Some optimizations are deterministic and won't benefit, but there are certainly plenty of optimizations that involve a search over some space of possibilities. An extreme version of that is the concept of "superoptimization", which optimizes a short code sequence by searching over all possible optimized versions and finding the one that is the fastest while remaining semantically equivalent to the original. See, e.g., the following papers:

R. Sausnauskas, Y. Chen, P. Collingbourne, J. Ketema, G. Lup, J. Taneja, J. Regehr. "A Synthesizing Superoptimizer."

Sorav Bansal, Alex Aiken. "Automatic Generation of Peephole Superoptimizers." ASPLOS 2006.