tweak compile_initial_prog to not emit a Stop instruction

and more importantly, strengthen its correctness theorem to show that
the generated bytecode will run to the end of the code