Make computation of number of arguments of opcode clearer

[franck44]

At the moment, the arguments of an instruction, e.g. PUSH1' are aseq`. In practice it must be of even length. This is an important assumption in the computation of the instruction following a given instruction:

• in the Splitter to display the next PC,
• in the computation of the address of the next block StartAddressNextSeg in LinSegments:

  function StartAddressNextSeg(): nat
  requires this.JUMPSeg? || this.CONTSeg?
  {
  this.lastIns.address + 1 + |this.lastIns.arg|/2
  }

To do

Add a constraint that the args in Instruction must have even length. This may be added to the IsValid() predicate.