Sui: Add invariant for Bytecode.t

[clarus]

Add an invariant for the Bytecode.t type in order to make the verify_instr_is_valid works.

It should look like:

Module Bytecode.
  Module Valid.
    Definition t (x : Bytecode.t) : Prop :=
      match x with
      | Bytecode.CastU16 => True
      ... (* most cases with `True` *)
      | Bytecode.VecPack _ z => Integer.Valid.t IntegerKind.U64 z
      (* sometimes with something else like above *)
      ...
      end.