uvmOptimizationsTheory proves the validity of optimizations on Mu
bytecode. Incomplete proofs are stubbed out with "cheat" or commented
out.