add special compile_initial_prog

for compiling a program that is known to succeed.
also prove half of its correctness theorem (cheat the part about
re-establishing the invariant; will prove later).