Use the `LENGTH ..._mc` expression to describe the byte length of a machine code

Using `LENGTH ..._mc` instead of putting the actual constant has two advantages:
- Even if the assembly is updated for some reason, the proof does not need to be updated.
- It helps reviewers because they do not need to double check whether the constants are correct. Also helps newbies to understand the specification.