No. 46 (2000): RS-46 Reasoning About Code-Generation in Two-Level Languages