Dexter verification

(Copy-cat of !69 (merged) that was accidentally merged.)

Related: #20 (closed) (overview, work division and progress)

Informal specification: https://docs.google.com/document/d/18bDwKlRuwAdsga8T5STpbNS-HGtyg8ST7MdAwTwpEQ8/edit?usp=sharing

Dexter contract in morley: https://gitlab.com/camlcase-dev/dexter/-/tree/master/dexter-contracts-morley

Structure of the ongoing verification effort:

• src/contracts_coq/dexter_string.v: Contains the dexter contract, the wip of the Morley version translated to michelson, as a string.
• src/contracts_coq/dexter_parse.v: Parses the string version of the contract, it's storage and parameter type to mi-cho-coq types. At some point, we need to check that the parsed and the hand-crafted versions are the same.
• src/contracts_coq/dexter_definition.v: contains the contract code, parameter and storage type. The contract and parameter types are split up into entry points. Each entrypoint has the type `entrypoint_parameter :: storage -> list operation :: storage`.
• src/contracts_coq/dexter_spec.v: Contains the specification of each entry points, and at the end the specification of the main function. The specification is based on the informal specification linked above. if there are questions on the formal specification, refer to the informal. you can put comments in the informal specification, and then ping James to have him answer.
• src/contracts_coq/dexter_verification.v: The correction proof will be put here. Ideally, Colin and Bruno will only need to modify this file. I've put lemmas for each entrypoint and the main file.

Practically, we might have to change this nice division of labor. Typically, we will notice that either the specification is incorrect or written in a way that is not practical for the proofs. I think it would be a good exercise to avoid editing the specification unless errors are found, but we'll see how the situation evolves.