We present a verifiable low-level program representation to embed,
propagate, and preserve safety information in high performance
compilers for safe languages such as Java and C#.  Our representation
precisely encodes safety information via static single-assignment
(SSA) proof variables that are first-class constructs in the program.

We argue that our representation allows a compiler to both (1) express
aggressively optimized machine-independent code and (2) leverage
existing compiler infrastructure to preserve safety information during
optimization.  We demonstrate that this approach supports standard
compiler optimizations, requires minimal changes to the implementation
of those optimizations, and does not artificially impede those
optimizations to preserve safety.

We also describe a simple type system that formalizes type safety in
an SSA-style control-flow graph program representation.  Through the
types of proof variables, our system enables compositional
verification of memory safety in optimized code.

Finally, we discuss experiences integrating this representation into
the machine-independent global optimizer of StarJIT, a
high-performance just-in-time compiler that performs aggressive
control-flow, data-flow, and algebraic optimizations and is
competitive with top production systems.