formalized bytecode conversions