Compiler verification is an important special case of program verification. It deals with correctness proofs of a program (compiler) that translate input programs into output programs. Barthe et al. tackle an interesting amalgam of the generic and specific by building a framework for translating proofs of assertions for source programs into equivalent proofs for the compiled programs.

The paper is set in the context of a proof-carrying code framework. It addresses the technical problem of generating proofs for programs that have undergone optimization transformations that induce, in general, transformations in both assertions and their proofs.

The paper assumes that a source program is already certified--that is, it already contains all necessary proofs for assertions--and that certifying analyzers exist that can generate proofs for analysis results. Another mild but technically crucial assumption made is that the programs are well annotated; this assumption induces an induction principle that is essential for proofs in the paper.

For each optimization step, assertions in the program are strengthened with program analysis information. Proofs of source program assertions are then translated into proofs of the strengthened properties in the optimized program. Barthe et al. show how this can be achieved for a range of optimizations, including function inlining, register allocation, and dead code elimination.

This paper’s mainly theoretical contribution is based on a simplistic register transfer language that is extended with assertions. It is well written and presents the basic concepts clearly. Barthe et al. are one step closer to the ultimate goal of trusted computing.