add more about the bytecode state to the invariant

about the labels, clock, and code execution