Draft: [dexter/fa2] add a hackish version of fa2 def/spec

I've copy-pasted the dexter development and updated the spec according to the dexter informal specification in the dexter-fa2 branch, specialized for the case where the target token contract is an FA2 contract: https://gitlab.com/camlcase-dev/dexter/-/blob/dexter-fa2/docs/dexter-informal-specification.md

In particular, this means that:

• the storage changes. instead of just storing the adress of the token contract, we also store a token id. this token id is constant. whenever a token_id is referred to in the Dexter/FA2 spec, it should refer to this one token id.
• the interactions with the token contract changes thus w.r.t. FA1.2:
  • the signature of transfer has changed and now takes a list of list of transfers, allowing batch transfers. in Dexter, transfer is always given an argument on the form [(from, [(to, (token_id, amount))])]
  • the getBalance is renamed balance_of, and its signature has changed. it now takes a a list [(owner, token_id), ... allowing the batched requests, looking up the balance of several owners with potentially different token_ids.
    • consequently, the signature of the callback changes, and now takes a list [((owner, token_id), balance)] where each element corresponds to the answer of one request in the original call to get_balance.
    • in the case of Dexter/FA2, the argument to balance_of is always a singleton list [(owner, token_id)]
  • thus the callback updateTokenPoolInternal changes as well. the logic is described in the informal spec

Currently, the branch has an updated spec and updated proofs.