Added some comments and state a theorem
-It's definitely missing assumptions (e.g. that next_alloc and
next_stack never clash with anything in the program)