A Provably Correct Stackless Intermediate Representation for Java Bytecode