Modifies the MIPS contracts to enforce that state.exited is either
exactly zero or one and cannot have any other value.