Formalize big maps
Currently big_map
s are simply map
s lacking iteration; to support TZT (issue #25) and to be future-proof (in particular with respect to https://gitlab.com/cryptiumlabs/tezos/-/merge_requests/146/), we need to formalize the internal format used in Tezos Michelson interpreter: a big map is either an index into a global storage of big_maps, a map literal, or a pair of an index and a diff (isomorphic to a map literal whose values are options).