Describir: Formal Verification of a Realistic Compiler.