Witnessing Program Transformations

We study two closely related problems: (a) showing that a program transformation is correct and (b) propagating a program invariant through a sequence of transformations. The second problem is motivated by an application where invariants on a program are used to enhance both the scope and the quality of the optimizations applied during compilation. We show that both problems can be addressed by generating, at compile-time, a witness for every instance of a transformation. A witness may be checked independently to establish the correctness of the transformation and, if correct, a witness helps transfer invariants from the source to the target program. This approach is simpler than proving correctness of the transformation over all inputs, and more comprehensive than translation validation heuristics, which are limited to specific transformations. We prove that stuttering simulation is a complete witness format: every correct transformation has a witness that is a stuttering simulation relation. Moreover, stuttering simulation witnesses compose, resulting in a single witness for a sequence of transformations. We define simulation witnesses for a number of standard compiler optimizations; this exercise indicates that witness generation is usually much simpler than the corresponding optimization procedure.