FA1.2 formalization and cross verification

See #40

This MR formalizes the FA1.2 specification, and verifies

• the Archetype implementation
• the camlCase implementation
• the Dexter2 implementation