Formalize serialization (PACK and UNPACK)
The PACK and UNPACK instructions are currently axiomatized.
The Micheline serialization is defined using Data_encoding, in https://gitlab.com/tezos/tezos/-/blob/master/src/lib_micheline/micheline.ml.
It has also been rewritten in a more direct style in a branch: https://gitlab.com/nomadic-labs/tezos/-/blob/klakplok+yrg@optimize-micheline-serialization.
Formalizing serialization is also required to use Concert + QuickChick.