Major refactoring to add contracts

- Labeling function uses state, not mock monad
- We have contracts & mon!
   - potential issue: because mons expand out into functions, if
statements, etc, they generate code. I add labels to this code on the
fly. I believe this will always terminate, but I’m not sure.